Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

BakelBdL18 (Article)
Author(s) Steffen van Bakel, Franco Barbanera and Ugo de' Liguoro
Title« Intersection Types for the lambda-mu Calculus »
JournalLogical Methods in Computer Science
Volume14
Number1
Year2018
URLhttp://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

BibTeX code

@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},
}


 Chronological Overview 
 Type-Hierarchical Overview 
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)

Valid HTML 4.01!