Extraction de code fonctionnel certifié à partir de spécifications inductives / Pierre-Nicolas Tollitte ; sous la direction de Catherine Dubois et de David Delahaye

Date :

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Catalogue Worldcat

Coq (logiciel)

Assistants de preuve

Théorie de la démonstration

Classification Dewey : 004

Dubois, Catherine (19..-.... ; informaticienne) (Directeur de thèse / thesis advisor)

Delahaye, David (1971-....) (Directeur de thèse / thesis advisor)

Leroy, Xavier (1968-.... ; chercheur en informatique) (Président du jury de soutenance / praeses)

Letouzey, Pierre (1977-....) (Rapporteur de la thèse / thesis reporter)

Rusu, Vlad (19..-.... ; informaticien) (Rapporteur de la thèse / thesis reporter)

Herbelin, Hugo (19..-....) (Membre du jury / opponent)

Jaume, Mathieu (Membre du jury / opponent)

Conservatoire national des arts et métiers (France) (Organisme de soutenance / degree-grantor)

École doctorale Informatique, télécommunications et électronique de Paris (Ecole doctorale associée à la thèse / doctoral school)

Centre d'études et de recherche en informatique et communications (Paris) (Laboratoire associé à la thèse / thesis associated laboratory)

Résumé / Abstract : Les outils d’aide à la preuve basés sur la théorie des types permettent à l’utilisateur d’adopter soit un style fonctionnel, soit un style relationnel (c’est-à-dire en utilisant des types inductifs). Chacun des deux styles a des avantages et des inconvénients. Le style relationnel peut être préféré parce qu’il permet à l’utilisateur de décrire seulement ce qui est vrai, de s’abstraire temporairement de la question de la terminaison, et de s’en tenir à une description utilisant des règles. Cependant, une spécification relationnelle n’est pas exécutable.Nous proposons un cadre général pour transformer une spécification inductive en une spécification fonctionnelle, en extrayant à partir de la première une fonction et en produisant éventuellement la preuve de correction de la fonction extraite par rapport à sa spécification inductive. De plus, à partir de modes définis par l’utilisateur, qui permettent de considérer les arguments de la relation comme des entrées ou des sorties (de fonction), nous pouvons extraire plusieurs comportements calculatoires à partir d’un seul type inductif.Nous fournissons également deux implantations de notre approche, l’une dans l’outil d’aide à la preuve Coq et l’autre dans l’environnement Focalize. Les deux sont actuellement distribuées avec leurs outils respectifs.

Résumé / Abstract : 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.