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