Travaux en Coq
Mémoire de DEA: Coq en Coq
Résumé:
L'étape essentielle de la certification d'un système de preuves tel
que Coq serait la vérification de son noyau: un vérificateur de
types d'un petit système de vérification de preuves basé sur le
Calcul des Constructions Inductives (CCI). Dans ce
papier, nous formalisons dans Coq la définition et la
métathéorie du Calcul des Constructions (CC), qui est un
fragment de CCI. En particulier, nous démontrons la normalisation
forte et la décidabilité du typage pour ce système. De
ce dernier résultat, un programme en Caml Light testant la
validité d'un jugement de typage dans le Calcul des
Constructions a été extrait. Ce programme intégré dans un système
comprenant un analyseur syntaxique et un pretty-printer est un
système de vérification de preuve autonome et performant pour le
Calcul des Constructions baptisé Coc. La preuve du lemme de
Newman produite avec Coq a pu être revérifiée dans Coc avec
des performances raisonables.
Documents accessibles:
Generalisation aux PTS avec sous-typage abstrait
Ce travail a été généralisé au cas des Systèmes de Types Purs avec
relation de sous-typage abstraite. Le développement en Coq se trouve
ici.
Thèse
Directeurs:
Gérard Huet et
Benjamin Werner
Subject:
Auto-validation d'un vérificateur de preuves avec familles inductives.
Rapport:
Version Postscript,
Référence BibTeX.
