Characterisation of Strongly Normalising lambda-mu-Terms

Steffen van Bakel
(Imperial College London, London, England)
Franco Barbanera
(Universita` di Catania, Catania, Italy)
Ugo de'Liguoro
(Universita` di Torino, Torino, Italy)

We provide a characterisation of strongly normalising terms of the lambda-mu-calculus by means of a type system that uses intersection and product types. The presence of the latter and a restricted use of the type omega enable us to represent the particular notion of continuation used in the literature for the definition of semantics for the lambda-mu-calculus. This makes it possible to lift the well-known characterisation property for strongly-normalising lambda-terms - that uses intersection types - to the lambda-mu-calculus. From this result an alternative proof of strong normalisation for terms typeable in Parigot's propositional logical system follows, by means of an interpretation of that system into ours.

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. 1–17.
Published: 30th July 2013.

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