Extraction in Coq: An Overview

13 years 4 months ago
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.
Pierre Letouzey
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where CIE
Authors Pierre Letouzey
Comments (0)