Synthesis of ML programs in the system Coq

The system Coq (Dowek et al., 1991) is an environment for proof development based on the Calculus of Constructions (Coquand, 1985) (Coquand and Huet, 1985) enhanced with inductive definitions (Coquand and Paulin-Mohring, 1990). From a constructive proof formalized in Coq, one extracts a functional program which can be compiled and executed in ML. This paper describes how to obtain ML programs from proofs in Coq. The methods are illustrated with the example of a propositional tautology checker. We study the specification of the problem, the development of the proof and the extraction of the executable ML program. Part of the example is the development of a normalization function for IF-expressions, whose termination has been studied in several formalisms (Leszczylowski, 1981) (Paulson, 1986) (Dybjer, 1990). We show that the total program using primitive recursive functionals obtained out of a structural proof of termination leads to an (at first) surprisingly efficient algorithm. We explain also how to introduce a fixpoint and get the usual recursive program. Optimizations which are necessary in order to obtain efficient programs from proofs will be explained. We also justify the properties of the final ML program with respect to the initial specification.