University of Birmingham > Talks@bham > Theoretical computer science seminar > Inductive-inductive definitions: axiomatisation and categorical semantics

## Inductive-inductive definitions: axiomatisation and categorical semanticsAdd to your list(s) Download to your calendar using vCal - Fredrik Nordvall Forsberg, Swansea University
- Friday 28 October 2011, 16:00-17:00
- LG52 Learning Centre.
If you have a question about this talk, please contact Paul Levy. Induction is a powerful and important principle of definition,
especially so in dependent type theory and constructive
mathematics. Induction-induction (named in reference to Dybjer and
Setzer’s induction-recursion) is an induction principle which gives
the possibility to simultaneously introduce a set A together with an
A-indexed set B (i.e. for every a : A, B(a) is a set). Both A and B
are inductively defined, and the constructors for A can refer to B and
vice versa. In addition, the constructors for B can also refer to the
In this talk, we consider some examples of inductive-inductive definitions. We then sketch a finite axiomatisation of the theory, and show how it can be given a categorical semantics similar to the initial algebra semantics of ordinary inductive data types. This talk is part of the Theoretical computer science seminar series. ## This talk is included in these lists:- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- LG52 Learning Centre
- Theoretical computer science seminar
- computer sience
Note that ex-directory lists are not shown. |
## Other listsLab Lunch Pure Détours Nuclear physics seminars## Other talksTBA Waveform modelling and the importance of multipole asymmetry in Gravitational Wave astronomy Ultrafast Spectroscopy and Microscopy as probes of Energy Materials Life : it’s out there, but what and why ? TBC Quantum Sensing in Space |