An intuitionistic λ-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 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.