an intuitionistic lambda calculus with exceptions

We introduce a typed lambda-calculus which allows the use of exceptions in the ML style. It is an extension of the system AF2 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 AF2. Moreover, the underlined logic of our system is intuitionistic logic.