CoqExtraction/LetouzeyOverview/1

#1 Introduction This article describes the current status of the extraction mechanism available in the Coq proof assistant [7, 8]. The extraction mechanism of Coq is a tool for automatic generation of programs out of Coq proofs and functions. These extracted programs are expressed in functional languages such as Ocaml, Haskell or Scheme, these three languages being the ones currently supported by Coq extraction. The main motivation for this extraction mechanism is to produce certied programs: each property proved in Coq will still be valid after extraction.

Through a series of examples about Euclidean division, we will review several alternatives that allow the user to express in Coq an algorithm that does not t naturally in this system. We will also see how these alternatives inuence the shape of the program obtained by extraction.We will then mention two advanced situations that illustrate the fact that Coq’s current extraction can handle any Coq objects, even the ones dened via high-end features of Coq and without direct counterpart in Ocaml or Haskell. We will summarize the key features of Coq extraction, mention some signicant Coq developments taking advantage of the extraction, and conclude on the current strengths of this tool, its limitations and future research perspectives.