Extracting Programs with Exceptions in an Impredicative Type System

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.

• Type: Conference
• Year: 1995
• Where: MPC
• Authors: Jean-François Monin
• Keywords: Classical Techniques, Impredicative Formalization, Mathematics, MPC 1995, Order Uni Cation