A Simple Calculus of Exception Handling

We introduce a simply-typed λ-calculus (λ→ exn ) featuring an ML-like exception handling mechanism. This calculus, whose type system corresponds to classical logic through the Curry-Howard isomorphism, satifies several interesting properties: among other, Church-Rosser, subject reduction, and strong-normalisation. Moreover, its typing system ensures that the reduction of well-typed expressions cannot give rise to uncaught exceptions.

• Type: Conference
• Year: 1995
• Where: TLCA
• Authors: Philippe de Groote
• Keywords: Curry-Howard Isomorphism, Exception Handling Mechanism, Theoretical Computer Science, TLCA 1995, Type System Corresponds