Bounding normalization time through intersection types

Erika De Benedetti
(Università degli Studi di Torino)
Simona Ronchi Della Rocca
(Università degli Studi di Torino)

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.

In Stéphane Graham-Lengrand and Luca Paolini: Proceedings Sixth Workshop on Intersection Types and Related Systems (ITRS 2012), Dubrovnik, Croatia, 29th June 2012, Electronic Proceedings in Theoretical Computer Science 121, pp. 48–57.
Published: 30th July 2013.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: