@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)