Characterisation of Strongly Normalising lambda-mu-Terms.
File(s)ITRS12.pdf (200.57 KB)
Published version
Author(s)
Bakel, SV
Barbanera, F
de'Liguoro, U
Type
Journal Article
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 Parigots propositional logical system follows, by means of an interpretation of that system into ours.
Date Issued
2013-07-30
Journal / Book Title
CoRR
Volume
abs/1307.8202
Copyright Statement
© 2013 The Authors
Description
23.06.14 KB. Ok to add published paper to spiral, author retain copyright