Skip to main content
PRL Project

Recursive Types in Coq

by Christine Paulin-Mohring

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.