PRL Seminars
Recursive Types in Coq
Christine Paulin-Mohring
Laboratoire de l'Informatique du Parallelisme,
CNRS URA 1398,
Ecole Normale Superieure de Lyon-FRANCE
Abstract
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.
Department of Computer Science, Cornell
University
|