|
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.
|