Extracting Programs with Exceptions in an Impredicative Type System
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 first 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 first order unification. Only small changes were needed in order to get a more efficient program from the original one.