Chapter 15: Execution of extracted programs in Caml and Haskell
Benjamin Werner and Jean-Christophe FilliātreIt is possible to use Coq to build certified and relatively efficient programs, extracting them from the proofs of their specifications. The extracted objects are terms of Fw, and can be obtained at the Coq toplevel with the command Extraction (see 15.1).
We present here a Coq module, Extraction, which translates the extracted terms to ML dialects, namely Caml Light, Objective Caml and Haskell. In the following, we will not refer to a particular dialect when possible and ``ML'' will be used to refer to any of the target dialects.
One builds effective programs in an Fw toplevel (actually the Coq toplevel) which contains the extracted objects and in which one can import ML objects. Indeed, in order to instantiate and realize Coq type and term variables, it is possible to import ML objects in the Fw toplevel, as inductive types or axioms.
Remark: The current mechanism of extraction of effective programs from Coq proofs slightly differs from the one in the versions of Coq anterior to the version V5.8. In these versions, there were an explicit toplevel for the language Fml. Moreover, it was not possible to import ML objects in this Fml toplevel.
In the first part of this document we describe the commands of the Extraction module, and we give some examples in the second part.