Rechercher

[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,

Auteurs: P. Tollitte

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: cpr

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:}",
}