An intuitionistic [lambda]-calculus with exceptions

Abstract

We introduce a typed λ-calculus which allows the use of exceptions in the ML style. It is an extension of the system $AF_2$ of Krivine & Leivant (Krivine, 1990; Leivant, 1983). We show its main properties: confluence, strong normalization and weak subject reduction. The system satisfies the “the proof as program” paradigm as in $AF_2$ . Moreover, the underlined logic of our system is intuitionistic logic.