University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Inductive-recursive definitions

Inductive-recursive definitions

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Sam Staton.

The slides for this talk are at

Inductive-recursive definitions were developed by P. Dybjer as a concepts which formalises the principle for introducing sets in Martin-Loef Type Theory. Indexed inductive-recursive definitions extend this principle by the possibility, to introduce simultaneously several sets inductive-recursively.

All sets definable in the core of Martin-Loef type theory, which is accepted by most researchers in this area, are instances of indexed inductive-recursive definitions. It contains as well many extensions, for instance Erik Palmgren’s superuniverses and higher universes. Many data types which are used in programming and theorem proving are instances of indexed inductive-recursive definitions, e.g. the accessible part of an ordering, Martin-Loef’s computability predicate, which was used in his normalisation proof for one version of Martin-Loef type theory, and Bove and Carpretta’s formalisation of partial functions in type theory.

In this lecture we will introduce the notions of inductive-recursive definitions and indexed inductive-recursive definitions. We will show how to introduce inductive-recursive defintions using finitely many rules. We look at the relationship between inductive-recursive definitions and initial algebras. We will then investigate new extensions of type theory, which look at first sight like inductive-recursive definitions, but are of different nature.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2020, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity