Introduction
- Nice introduction to the type theory
- Lectures about Coq
Metatheory of the Calculus of Constructions
Metatheory of Inductive Types
Definitions and further issues regarding inductive types in Coq, Christine Paulin (in French)
In this work the definitions based on case (case analysis, now called match) and Fixpoint are described. Several issues eg. mutual inductive types, restrictions on elimination sort and positivity condition are studied.
Guardedness condition for fixed points and cofixed points, Eduardo Giménez
Model Construction
Realizability model for the calculus of construction with universes (CC_{omega}) with subtyping, Alexandre Miquel This paper contains realizability model for a system stronger than Coq but without inductive types.
(In)dependence of Axioms
Groupoid model of intensional Martin-Lof type theory, Martin Hofmann and Thomas Streicher: This shows the independence of Axiom K, which states that there is only one proof of reflexivity statement.
Others
Why does Coq use inductive types and not W-Types?