A Simple Calculus of Exception Handling Philippe

Abstract. 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.