Steffen van Bakel ; Franco Barbanera ; Ugo de'Liguoro - Intersection Types for the lambda-mu Calculus

lmcs:4194 - Logical Methods in Computer Science, January 10, 2018, Volume 14, Issue 1 - https://doi.org/10.23638/LMCS-14(1:2)2018
Intersection Types for the lambda-mu CalculusArticle

Authors: Steffen van Bakel ; Franco Barbanera ; Ugo de'Liguoro

    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.


    Volume: Volume 14, Issue 1
    Published on: January 10, 2018
    Accepted on: January 10, 2018
    Submitted on: January 10, 2018
    Keywords: Computer Science - Logic in Computer Science,F.4,F.4.1

    Consultation statistics

    This page has been seen 1510 times.
    This article's PDF has been downloaded 321 times.