Coq in Coq
Proofs in Coq
Definition of terms
Confluence of CC, Church-Rosser
Metatheory of CC
Strengthening lemma
Type approximation
Kind Skeletons
Reducibility Candidates
Interpretation of terms and types
Strong Normalization Theorem
Decidability of conversion
Decidability of typing
Logical Consistency
Extraction
Table of contents
General Lemmas
Additional results on lists
Caml Programs
Extracted program
Kernel of Coc
Example: Newman's lemma in Coc
Proof listing