Exceptions considered harmless

AbstractProgram extraction is a well known technique for developing correct functional programs from a constructive proof of their specification. This paper shows how to deal with exceptions in such a framework. We propose a modular (and impredicative) formalization in the calculus of constructions and we illustrate the technique on three examples