Extraction in Coq: An Overview

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.

• Type: Conference
• Year: 2008
• Where: CIE
• Authors: Pierre Letouzey
• Keywords: Applied Computing, CIE 2008, Coq Denitions, Coq Proofs, Extraction Mechanism