BakelBdL18 (Article)

Author(s)  Steffen van Bakel, Franco Barbanera and Ugo de' Liguoro 
Title  « Intersection Types for the lambdamu 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 lambdamu 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 omegaalgebraic lattices via Abramsky's domainlogic 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 lambdamu term is typeable if and only if it is strongly normalising. We also show that Parigot's typing of lambdamu 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 lambdamu 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 lambdamu Calculus}},
abstract = {We introduce an intersection type system for the lambdamu
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
omegaalgebraic lattices via Abramsky's domainlogic 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 lambdamu term is typeable if and only if it is strongly
normalising. We also show that Parigot's typing of lambdamu 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 lambdamu
calculus.},
tag = {Logical Methods in Computer Science},
journal = {{Logical Methods in Computer Science}},
year = {2018},
doi = {DOI:10.23638/LMCS14(1:2)2018},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)