Subset Coercions in Coq Export

@incollection{sozeau:scic, abstract = {We propose a new language for writing programs with dependent types on top of the Coq proof assistant. This language permits to establish a phase distinction between writing and proving algorithms in the Coq environment. Concretely, this means allowing to write algorithms as easily as in a practical functional programming language whilst giving them as rich a specification as desired and proving that the code meets the specification using the whole Coq proof apparatus. This is achieved by extending conversion to an equivalence which relates types and subsets based on them, a technique originating from the ” Predicate subtyping” feature of PVS and following mathematical convention. The typing judgements can be translated to the (CIC) by means of an interpretation which inserts coercions at the appropriate places. These coercions can contain existential variables representing the propositional parts of the final term, corresponding to proof obligations (or PVS type-checking conditions). A prototype implementation of this process is integrated with the Coq environment.}, author = {Sozeau, Matthieu}, booktitle = {Types for Proofs and Programs}, citeulike-article-id = {2443518}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-540-74464-1_16}, citeulike-linkout-1 = {http://www.springerlink.com/content/8p35448426n2n41k}, doi = {10.1007/978-3-540-74464-1_16}, editor = {Altenkirch, Thorsten and Mcbride, Conor}, journal = {Types for Proofs and Programs}, keywords = {coq, dependent-types, functional-programming, theorem-proving, type-theory}, pages = {237--252}, posted-at = {2008-02-28 13:56:18}, priority = {4}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Subset Coercions in Coq}, url = {http://dx.doi.org/10.1007/978-3-540-74464-1_16}, year = {2007} }

TY - CHAP ID - sozeau:scic L3 - citeulike-article-id:2443518 N2 - We propose a new language for writing programs with dependent types on top of the Coq proof assistant. This language permits to establish a phase distinction between writing and proving algorithms in the Coq environment. Concretely, this means allowing to write algorithms as easily as in a practical functional programming language whilst giving them as rich a specification as desired and proving that the code meets the specification using the whole Coq proof apparatus. This is achieved by extending conversion to an equivalence which relates types and subsets based on them, a technique originating from the “Predicate subtyping” feature of PVS and following mathematical convention. The typing judgements can be translated to the (CIC) by means of an interpretation which inserts coercions at the appropriate places. These coercions can contain existential variables representing the propositional parts of the final term, corresponding to proof obligations (or PVS type-checking conditions). A prototype implementation of this process is integrated with the Coq environment. JF - Types for Proofs and Programs SE - Lecture Notes in Computer Science EP - 252 TI - Subset Coercions in Coq PB - Springer T2 - Types for Proofs and Programs SP - 237 KW - coq KW - dependent-types KW - functional-programming KW - theorem-proving KW - type-theory AU - Sozeau, Matthieu A2 - Altenkirch, Thorsten A2 - Mcbride, Conor PY - 2007/// UR - http://dx.doi.org/10.1007/978-3-540-74464-1_16 ER -