Bounding normalization time through intersection types

Non-idempotent intersection types are used in order to give a bound of the length of the normalization beta-reduction sequence of a lambda term: namely, the bound is expressed as a function of the size of the term.

Saved in:
Bibliographic Details
Published in:Electronic proceedings in theoretical computer science 2013-07, Vol.121 (Proc. ITRS 2012), p.48-57
Main Authors: De Benedetti, Erika, Ronchi Della Rocca, Simona
Format: Article
Language:English
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Non-idempotent intersection types are used in order to give a bound of the length of the normalization beta-reduction sequence of a lambda term: namely, the bound is expressed as a function of the size of the term.
ISSN:2075-2180
2075-2180
DOI:10.4204/EPTCS.121.4