Sylvain Lebresne - A Type System For Call-By-Name Exceptions

lmcs:817 - Logical Methods in Computer Science, November 2, 2009, Volume 5, Issue 4 -
A Type System For Call-By-Name Exceptions

Authors: Sylvain Lebresne

    We present an extension of System F with call-by-name exceptions. The type system is enriched with two syntactic constructs: a union type for programs whose execution may raise an exception at top level, and a corruption type for programs that may raise an exception in any evaluation context (not necessarily at top level). We present the syntax and reduction rules of the system, as well as its typing and subtyping rules. We then study its properties, such as confluence. Finally, we construct a realizability model using orthogonality techniques, from which we deduce that well-typed programs are weakly normalizing and that the ones who have the type of natural numbers really compute a natural number, without raising exceptions.

    Volume: Volume 5, Issue 4
    Published on: November 2, 2009
    Accepted on: June 25, 2015
    Submitted on: January 9, 2009
    Keywords: Computer Science - Programming Languages,D.3.1,F.4.1

    2 Documents citing this article


    Consultation statistics

    This page has been seen 287 times.
    This article's PDF has been downloaded 271 times.