Coq en Coq
Preuves en Coq
Définition des Termes
Confluence de CC, Church-Rosser
Métatheorie de CC
Approximations de Types
Squelettes d'Ordres
Candidats de Réductibilité
Interprétation des Termes et des Types
Théorème de Normalisation Forte
Décidabilité de la Conversion
Décidabilité du Typage
Extraction
Lemmes Généraux
Résultats Complémentaires sur les Listes
Logique dans Type
Programmes en Caml
Programme Extrait
Noyau Coc
Exemple: le Lemme de Newman en Coc
Listing de la Preuve