Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

12

CIE
2008
Springer

favoriteEmaildiscussreport

114views Applied Computing» more CIE 2008»

Extraction in Coq: An Overview

13 years 6 months ago

Extraction in Coq: An Overview

Download hal.archives-ouvertes.fr

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

Real-time Traffic

Applied Computing | CIE 2008 | Coq Denitions | Coq Proofs | Extraction Mechanism |

claim paper

Related Content

» Extracting a Data Flow Analyser in Constructive Logic

» Automatic Complexity Analysis for Programs Extracted from Coq Proof

» Formal Verification of a C Compiler FrontEnd

» Building Certified Static Analysers by Modular Construction of Wellfounded Lattices

» Tilting at Windmills with Coq Formal Verification of a Compilation Algorithm for Parallel ...

» Formal correctness of conflict detection for firewalls

» A LargeScale Experiment in Executing Extracted Programs

» TRX A Formally Verified Parser Interpreter

» Program Extraction from Normalization Proofs

Post Info
More Details (n/a)

Added	12 Oct 2010
Updated	12 Oct 2010
Type	Conference
Year	2008
Where	CIE
Authors	Pierre Letouzey

Comments (0)