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


Consultation statistics

This page has been seen 250 times.
This article's PDF has been downloaded 240 times.