COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

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

## Inductive-recursive definitionsAdd 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
- Computer Laboratory talks
- Computing and Mathematics
- 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. |
## Other listsCoffee with Scientists Building Bridges in Medical Science Conference Greece and its History## Other talksRefugees and Migration Finding the past: Medieval Coin Finds at the Fitzwilliam Museum Polish Britain: Multilingualism and Diaspora Community SciBar: Sleep, Dreams and Consciousness Satellite Observations for Climate Resilience and Sustainability How to write good papers 'Ways of Reading, Looking, and Imagining: Contemporary Fiction and Its Optics' Single Cell Seminars (August) Knot Floer homology and algebraic methods The ‘Easy’ and ‘Hard’ Problems of Consciousness Constructing datasets for multi-hop reading comprehension across documents |