Vers une certification de l'extraction de coq
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
The Coq proof assistant mechanically checks the consistency of the logical reasoning in a proof. It can also be used to develop certified programs. Indeed, Coq uses intemally a typed language derived from lambda-calculus, the calculus of inductive constructions (CIC). This language can be directl; used by a programmer, and a procedure, extraction, allows one to translate CIC programs into more widely used languages such as OCaml, Haskell or Scheme. Extraction is not a mere syntax change: the type System of CIC is very rich, but purely logical entities can appear inside programs, impacting their performance. Extraction erases these logical artefacts as well. In this thesis, we tackle certification of the extraction itself. We have proved its correction in the context of a full formalization of Coq in Coq. Even though this formalization is not exactly Coq, we worked on it with the concrete implementation of Coq in mind. We also propose a new way to certify extracted programs, in the concrete setting of the existing Coq System.
Abstract FR:
L'assistant de preuve Coq permet de s'assurer mécaniquement de la correction de chaque étape de raisonnement dans une preuve. Ce système peut également servir au développement de programmes certifiés. En effet, Coq utilise en interne un langage typé dérivé du lambda-calcul, le calcul des constructions inductives (CIC). Ce langage est directement utilisable pour programmer, et un mécanisme, l'extraction, permet de traduire les programmes CIC vers des langages à plus large audience tels qu'OCaml, Haskell ou Scheme. L'extraction n'est pas un simple changement de syntaxe: CIC dispose d'un système de types très riche, mais en contrepartie, des entités purement logiques peuvent apparaître dans les programmes et impacter leurs performances. L'extraction se charge également d'effacer ces parties logiques. Dans cette thèse, nous nous attaquons à la certification de l'extraction elle-même. Nous avons prouvé sa correction dans le cadre d'une formalisation entière de Coq en Coq. Cette formalisation ne correspond pas exactement au CIC implanté dans Coq, mais nous avons tout de même réalisé notre étude avec l'implantation concrète de Coq en tête. Nous proposons également une nouvelle méthode de certification des programmes extraits, dans le cadre concret du système Coq existant.