Lebresne, Sylvain - 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: Lebresne, Sylvain

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.


Source : oai:arXiv.org:0907.2059
DOI : 10.2168/LMCS-5(4:1)2009
Volume: Volume 5, Issue 4
Published on: November 2, 2009
Submitted on: January 9, 2009
Keywords: Computer Science - Programming Languages,D.3.1,F.4.1


Share

Consultation statistics

This page has been seen 49 times.
This article's PDF has been downloaded 47 times.