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