Intersection types for the λμ-calculus
File(s)LMCS.pdf (2.22 MB)
Published version
Author(s)
van Bakel, Steffen
Barbanera, Franco
de'Liguoro, Ugo
Type
Journal Article
Abstract
We introduce an intersection type system for the lambda-mu calculus that is invariant under subject reduction and expansion. The system is obtained by describing Streicher and Reus's denotational model of continuations in the category of omega-algebraic lattices via Abramsky's domain-logic approach. This provides at the same time an interpretation of the type system and a proof of the completeness of the system with respect to the continuation models by means of a filter model construction. We then define a restriction of our system, such that a lambda-mu term is typeable if and only if it is strongly normalising. We also show that Parigot's typing of lambda-mu terms with classically valid propositional formulas can be translated into the restricted system, which then provides an alternative proof of strong normalisability for the typed lambda-mu calculus.
Date Issued
2018-01-10
Date Acceptance
2018-01-10
Citation
Logical Methods in Computer Science (LMCS), 2018, 14 (1)
ISSN
1860-5974
Publisher
Technical University of Braunschweig
Journal / Book Title
Logical Methods in Computer Science (LMCS)
Volume
14
Issue
1
Copyright Statement
© 2018 Owner. This an open access article distributed under the terms of the Creative Commons Attribution 4.0, which permits redistribution and copy for non-commercial use, provided the original article is not altered, and the author(s) and source is credited. http://creativecommons.org/licenses/by/4.0/.
License URL
Subjects
0101 Pure Mathematics
0802 Computation Theory and Mathematics
0803 Computer Software
Publication Status
Published
Date Publish Online
2018-01-10