Sciweavers

MPC
1995
Springer

Extracting Programs with Exceptions in an Impredicative Type System

14 years 3 months ago
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.
Jean-François Monin
Added 26 Aug 2010
Updated 26 Aug 2010
Type Conference
Year 1995
Where MPC
Authors Jean-François Monin
Comments (0)