BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:A Fibrational Induction Rule for Inductive Types -
Patricia Johann\, University of Strathclyde
DTSTART:20100504T120000Z
DTEND:20100504T130000Z
UID:TALK372AT
URL:/talk/index/372
DESCRIPTION:We develop a generic induction rule that can be us
ed to prove properties of inductive data types. Ou
r results are semantic in nature and are inspired
by Hermida and Jacobs' elegant algebraic formulati
on of induction for polynomial data types. Our co
ntribution is to derive\, under slightly different
assumptions\, an induction rule that is generic o
ver _all_ inductive types\, polynomial or not. Ou
r induction rule is generic over the kinds of prop
erties to be proved as well over the data types to
which the properties refer. Like Hermida and Jaco
bs\, we work in a general fibrational setting and
so can accommodate very general notions of propert
ies on inductive types rather than just those of p
articular syntactic forms. The correctness of our
generic induction rule is proved by reducing induc
tion to iteration. We show how our rule can be ins
tantiated to give induction rules for non-polynomi
al data types such as rose trees\, finite heredita
ry sets\, and hyperfunctions. Our instantiation fo
r hyperfunctions underscores the value of working
in the general fibrational setting since this data
type cannot be interpreted as a set.\n\nThis is j
oint work with Neil Ghani and Clement Fumex.
LOCATION:Venue to be confirmed
CONTACT:Paul Levy
END:VEVENT
END:VCALENDAR