Publications

BibTex format

@article{van:2018:10.23638/LMCS-14(1:2)2018,
author = {van, Bakel S and Barbanera, F and de'Liguoro, U},
doi = {10.23638/LMCS-14(1:2)2018},
journal = {Logical Methods in Computer Science (LMCS)},
title = {Intersection types for the λμ-calculus},
url = {http://dx.doi.org/10.23638/LMCS-14(1:2)2018},
volume = {14},
year = {2018}
}

Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - 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.
AU  - van,Bakel S
AU  - Barbanera,F
AU  - de'Liguoro,U
DO  - 10.23638/LMCS-14(1:2)2018
PY  - 2018///
SN  - 1860-5974
TI  - Intersection types for the λμ-calculus
T2  - Logical Methods in Computer Science (LMCS)
UR  - http://dx.doi.org/10.23638/LMCS-14(1:2)2018
UR  - http://hdl.handle.net/10044/1/83271
VL  - 14
ER  -

Download

DrSteffenvan Bakel

Contact

Location

Summary

Citation

BibTex format

RIS format (EndNote, RefMan)