Abstract. This paper is about exceptions handling using classical techniques of program extraction. We propose an impredicative formalization in the calculus of constructions and we illustrate the technique on two examples. The rst one, though simple, allows us to experiment various techniques. The second one is an adaptation of a bigger algorithm previously developed in Coq by J. Rouyer, namely rst order uni cation. Only small changes were needed in order to get a more e cient program from the original one.