## 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?

A summary of the long and informative discussion that took place on the coq-club mailing list when similar bugs were discovered in the termination checkers of both Coq and Agda.

Some proof theoretic consequences of impredicative Prop.