|
 
|
[TDD12] Producing Certified Functional Code from Inductive Specifications
Conférence Internationale avec comité de lecture : International Conference on Certified Programs and Proofs (CPP 2012), December 2012, Vol. 7679, pp.76-91, Series LNCS, Kyoto, Japan,Mots clés: extraction, inductive types, Coq
Résumé:
Proof assistants based on type theory allow the user to adopt either a functional style, or a relational style (e.g., by using inductive types). Both styles have pros and cons. Relational style may be pre- ferred because it allows the user to describe only what is true, discard momentarily the termination question, and stick to a rule-based descrip- tion. However, a relational specification is usually not executable. This paper proposes to turn an inductive specification into a functional one, in the logical setting itself, more precisely Coq in this work. We define for a certain class of inductive specifications a way to extract functions from them and automatically produce the proof of soundness of the extracted function w.r.t. its inductive specification. In addition, using user-defined modes which label inputs and outputs, we are able to extract several computational contents from a single inductive type.
Equipe:
sys
BibTeX
| @inproceedings { | |||
| TDD12, | |||
| title | = | "{Producing Certified Functional Code from Inductive Specifications}", | |
| author | = | " P. Tollitte and D. Delahaye and C. Dubois ", | |
| booktitle | = | "{International Conference on Certified Programs and Proofs (CPP 2012)}", | |
| year | = | 2012, | |
| edition | = | "Springer", | |
| month | = | "December", | |
| series | = | "LNCS", | |
| volume | = | 7679, | |
| pages | = | "76-91", | |
| address | = | "Kyoto, Japan", | |
| } | |||
