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.

Recursive Types in Coq

by Christine Paulin-Mohring 1994-1995

by Christine Paulin-Mohring
1994-1995