BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Inductive-recursive definitions - Anton Setzer (University of Swan
 sea)
DTSTART:20090529T130000Z
DTEND:20090529T140000Z
UID:TALK17510@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:The slides for this talk are at http://www.cs.swan.ac.uk/~cset
 zer/slides/index.html. \n\nInductive-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 e
 xtend this principle by the possibility\, to introduce simultaneously seve
 ral sets inductive-recursively.\n\nAll sets definable in the core of Marti
 n-Loef type theory\, which is accepted by most researchers in this area\, 
 are instances of indexed inductive-recursive definitions. It contains as w
 ell many extensions\, for instance Erik Palmgren's superuniverses and high
 er universes. Many data types which are used in programming and theorem pr
 oving are instances of indexed inductive-recursive definitions\, e.g. the 
 accessible part of an ordering\, Martin-Loef's computability predicate\, w
 hich was used in his normalisation proof for one version of Martin-Loef ty
 pe theory\, and Bove and Carpretta's formalisation of partial functions in
  type theory.\n\nIn this lecture we will introduce the notions of inductiv
 e-recursive definitions and indexed inductive-recursive definitions. We wi
 ll show how to introduce inductive-recursive defintions using finitely man
 y rules. We look at the relationship between inductive-recursive definitio
 ns and initial algebras. We will then investigate new extensions of type t
 heory\, which look at first sight like inductive-recursive definitions\, b
 ut are of different nature.\n\n
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR