|
Formal Methods in Computing (Most of the papers antecedent to 1995 are not included in the list) |
|||
| FRAMES NO FRAME | ||||
| vBBdL-2014 (Unpublished) | |
| Author(s) | Steffen van Bakel, Franco Barbanera and Ugo de' Liguoro |
| Title | « Intersection Types for the lambda-mu Calculus » |
| Abstract | |
| We introduce an intersection type system for the pure lambda-mu calculus, which 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 do- main 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 ours 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. | |
Download the complete article:
| BibTeX code |
@unpublished{vBBdL-2014,
localfile = {http://www.di.unito.it/~deligu/papers/lmcs-IntTypeLmu.pdf},
abstract = {We introduce an intersection type system for the pure lambda-mu
calculus, which 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 do- main 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 ours 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.},
title = {{Intersection Types for the lambda-mu Calculus}},
author = {Steffen van Bakel and Franco Barbanera and Ugo de' Liguoro},
year = {2014},
}
|
Formal Methods in Computing (Most of the papers antecedent to 1995 are not included in the list) |
|||
| FRAMES NO FRAME | ||||
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)
