A New Extraction for Coq Export

@incollection{letouzey:anefc, abstract = {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.}, author = {Letouzey, Pierre}, citeulike-article-id = {2429849}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/3-540-39185-1_12}, doi = {10.1007/3-540-39185-1_12}, journal = {Types for Proofs and Programs}, keywords = {coq, dependent-types, type-theory}, pages = {617}, posted-at = {2008-04-29 16:34:53}, priority = {1}, title = {A New Extraction for Coq}, url = {http://dx.doi.org/10.1007/3-540-39185-1_12}, year = {2003} }

TY - CHAP ID - letouzey:anefc L3 - citeulike-article-id:2429849 N2 - 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. JF - Types for Proofs and Programs EP - 617 TI - A New Extraction for Coq SP - 617 KW - coq KW - dependent-types KW - type-theory AU - Letouzey, Pierre PY - 2003/// UR - http://dx.doi.org/10.1007/3-540-39185-1_12 ER -