|
 
|
[Tol13] Extraction de code fonctionnel certifié à partir de spécifications inductives
Mémoire de Thèse : Soutenue le: 06 December 2013, pp. 180, pp.: Directeur:Rapporteur 1:
Rapporteur 2:
Membre du jury:
Membre du jury:
Membre du jury:, : Extraction de code fonctionnel certifié à partir de spécifications inductives,
Mots clés: Executable specifications, inductive relations, functional code generation, proof generation, Coq, Focalize.
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 advantages and
drawbacks. Relational style may be preferred because it allows the user to describe only
what is true, discard momentarily the termination question, and stick to a rule-based
description. However, a relational specification is usually not executable.
We propose a general framework to turn an inductive specification into a functional one, by
extracting a function from the former and eventually 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.
We also provide two implementations of our approach, one in the Coq proof assistant and
the other in the Focalize environnement. Both are currently distributed with the respective
tools.
Equipe:
sys
BibTeX
| @phdthesis { | |||
| Tol13, | |||
| title | = | "{Extraction de code fonctionnel certifié à partir de spécifications inductives}", | |
| author | = | "P. Tollitte", | |
| year | = | 2013, | |
| pages | = | "180", | |
| address | = | "{CEDRIC Laboratory, Paris, France}", | |
| note | = | "{ Directeur: Rapporteur 1: Rapporteur 2: Membre du jury: Membre du jury: Membre du jury:}", | |
| } |
