CoqExtraction/LetouzeyOverview

#Extraction in Coq: an Overview Pierre Letouzey

Laboratoire PPS, Université Paris Diderot - Paris 7 Case 7014, F-75205 Paris Cedex 13, France

letouzey@pps.jussieu.fr

Abstract. The extraction mechanism of Coq allows one to transform Coq proofs and functions into functional programs. We illustrate the behavior of this tool by reviewing several variants of Coq denitions for Euclidean division, as well as some more advanced examples. We then continue with a more general description of this tool: key features, main examples, strengths, limitations and perspectives.

##Table of contents - 1. Introduction - 2. Extraction in practive : div - 3. Examples beyond ML type system - 4. Key features of extraction - 5. Some significant Coq developments using extraction - 6. Conclusion and future works