Characterisation of Approximation and (Head) Normalisation for λμ using Strict Intersection Types

Steffen van Bakel
(Imperial College London, UK)

We study the strict type assignment for lambda-mu that is presented in [van Bakel'16]. We define a notion of approximants of lambda-mu-terms, show that it generates a semantics, and that for each typeable term there is an approximant that has the same type. We show that this leads to a characterisation via assignable types for all terms that have a head normal form, and to one for all terms that have a normal form, as well as to one for all terms that are strongly normalisable.

In Naoki Kobayashi: Proceedings Eighth Workshop on Intersection Types and Related Systems (ITRS 2016), Porto, Portugal, 26th June 2016, Electronic Proceedings in Theoretical Computer Science 242, pp. 20–30.
Published: 7th February 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.242.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org