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

Inductive-inductive definitions: axiomatisation and categorical semantics

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

  • UserFredrik Nordvall Forsberg, Swansea University
  • ClockFriday 28 October 2011, 16:00-17:00
  • HouseLG52 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 constructors for A.

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.