A new extraction for Coq
In: TYPES 2002 : types for proofs and programs (Berg en Dal, 24-28 April 2002, selected papers)Lecture notes in computer science; (2003) S. 200-219
Konferenz
- print, 18 ref
Zugriff:
We present here a new extraction mechanism for the Coq proof assistant [17]. By extraction, we mean automatic generation of functional code from Coq proofs, in order to produce certified programs. In former versions of Coq, the extraction mechanism suffered several limitations and in particular worked only with a subset of the language. We first discuss difficulties encountered and solutions proposed to remove these limitations. Then we give a proof of correctness for a theoretical model of the new extraction. Finally we describe the actual implementation distributed in Coq version 7.3 and further.
Titel: |
A new extraction for Coq
|
---|---|
Autor/in / Beteiligte Person: | LETOUZEY, Pierre |
Link: | |
Quelle: | TYPES 2002 : types for proofs and programs (Berg en Dal, 24-28 April 2002, selected papers)Lecture notes in computer science; (2003) S. 200-219 |
Veröffentlichung: | Berlin: Springer, 2003 |
Medientyp: | Konferenz |
Umfang: | print, 18 ref |
ISSN: | 0302-9743 (print) |
Schlagwort: |
|
Sonstiges: |
|