Inductive-recursive definitions

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

• Anton Setzer (University of Swansea)
• Friday 29 May 2009, 14:00-15:00
• Room FW11, Computer Laboratory, William Gates Building.

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

The slides for this talk are at http://www.cs.swan.ac.uk/~csetzer/slides/index.html.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• Room FW11, Computer Laboratory, William Gates Building
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.