BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:Inductive-recursive definitions - Anton Setzer (Un
iversity of Swansea)
DTSTART;TZID=Europe/London:20090529T140000
DTEND;TZID=Europe/London:20090529T150000
UID:TALK17510AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/17510
DESCRIPTION:The slides for this talk are at http://www.cs.swan
.ac.uk/~csetzer/slides/index.html. \n\nInductive-r
ecursive definitions were developed by P. Dybjer a
s a concepts which formalises the principle for in
troducing sets in Martin-Loef Type Theory. Indexed
inductive-recursive definitions extend this princ
iple by the possibility\, to introduce simultaneou
sly several sets inductive-recursively.\n\nAll set
s definable in the core of Martin-Loef type theory
\, which is accepted by most researchers in this a
rea\, 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 i
n programming and theorem proving are instances of
indexed inductive-recursive definitions\, e.g. th
e accessible part of an ordering\, Martin-Loef's c
omputability predicate\, which was used in his nor
malisation 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 l
ecture we will introduce the notions of inductive-
recursive definitions and indexed inductive-recurs
ive definitions. We will show how to introduce ind
uctive-recursive defintions using finitely many ru
les. We look at the relationship between inductive
-recursive definitions and initial algebras. We wi
ll then investigate new extensions of type theory\
, which look at first sight like inductive-recursi
ve definitions\, but are of different nature.\n\n
LOCATION:Room FW11\, Computer Laboratory\, William Gates Bu
ilding
CONTACT:Sam Staton
END:VEVENT
END:VCALENDAR