BakelBdL18 (Article)
|
Author(s) | Steffen van Bakel, Franco Barbanera and Ugo de' Liguoro |
Title | « Intersection Types for the lambda-mu Calculus » |
Journal | Logical Methods in Computer Science |
Volume | 14 |
Number | 1 |
Year | 2018 |
URL | http://lmcs.episciences.org/4194 |
Abstract & Keywords |
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.
Keywords: Computer Science - Logic in Computer Science ; F.4 ; F.4.1
|
@article{BakelBdL18,
number = 1,
volume = 14,
author = {Steffen van Bakel and Franco Barbanera and Ugo de' Liguoro},
keywords = {Computer Science - Logic in Computer Science ; F.4 ; F.4.1},
timestamp = {Wed, 07 Jun 2017 14:40:56 +0200},
url = {http://lmcs.episciences.org/4194},
title = {{Intersection Types for the lambda-mu Calculus}},
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.},
tag = {Logical Methods in Computer Science},
journal = {{Logical Methods in Computer Science}},
year = {2018},
doi = {DOI:10.23638/LMCS-14(1:2)2018},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)