Characterisation of Strongly Normalising lambda-mu-Terms
Abstract
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.
Keywords
Cite
@article{arxiv.1307.8202,
title = {Characterisation of Strongly Normalising lambda-mu-Terms},
author = {Steffen van Bakel and Franco Barbanera and Ugo de'Liguoro},
journal= {arXiv preprint arXiv:1307.8202},
year = {2013}
}
Comments
In Proceedings ITRS 2012, arXiv:1307.7849