Coq in Coq

Proofs in Coq

• Definition of terms
• Confluence of CC, Church-Rosser
• Metatheory of CC
• Type approximation
• Kind Skeletons
• Reducibility Candidates
• Interpretation of terms and types
• Strong Normalization Theorem
• Decidability of conversion
• Decidability of typing
• Extraction

General Lemmas

• Additional results on lists
• Logic fragment in Type

Caml Programs

• Extracted program
• Kernel of Coc

Example: Newman's lemma in Coc

• Proof listing