|
|
From the latter proof, we extract a certified Caml Light program, which performs type inference (or type-checking) for an arbitrary typing judgement in CC. Integrating this program in a larger system, including a parser and pretty-printer, we obtain a stand-alone proof-checker, called CoC, for the Calculus of Constructions.
|
|
|
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.
|
