[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


@inproceedings {
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)}",
address="Kyoto, Japan",