Recursive Types in Coq
by Christine Paulin-Mohring
Laboratoire de l'Informatique du Parallelisme,
CNRS URA 1398,
Ecole Normale Superieure de Lyon-FRANCE
The theory of the proof assistant Coq is based on the Calculus of Constructions extended with a general mechanism for inductive definition of types and relations. The purpose of this talk is to discuss the representation of these inductive definitions in Coq.
More precisely, we shall present the motivations of such a calculus and the theoretical results known about it. We shall also discuss the new rules for elimination of inductive families proposed by Thierry Coquand.