Intersection Types for Unboundedness Problems

Paweł Parys
(Institute of Informatics, University of Warsaw)

Intersection types have been originally developed as an extension of simple types, but they can also be used for refining simple types. In this survey we concentrate on the latter option; more precisely, on the use of intersection types for describing quantitative properties of simply typed lambda-terms. We present two type systems. The first allows to estimate (by appropriately defined value of a derivation) the number of appearances of a fixed constant 'a' in the beta-normal form of a considered lambda-term. The second type system is more complicated, and allows to estimate the maximal number of appearances of the constant 'a' on a single branch.

Invited Presentation in Michele Pagani and Sandra Alves: Proceedings Twelfth Workshop on Developments in Computational Models and Ninth Workshop on Intersection Types and Related Systems (DCM 2018 and ITRS 2018 ), Oxford, UK, 8th July 2018, Electronic Proceedings in Theoretical Computer Science 293, pp. 7–27.
Published: 23rd April 2019.

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