# * Recursive Types in Coq *

## by Christine Paulin-Mohring

1994-1995

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.