BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The structures of induction and co-induction. - Paul Downen\, Univ
 ersity of Oregon.
DTSTART:20150917T140000Z
DTEND:20150917T150000Z
UID:TALK60937@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:We know that induction and co-induction are two sides of the s
 ame coin. So why do our proof assistants and dependently typed languages\,
  like Coq and Agda\, support induction better than co-induction? The root 
 of this bias grows out of missing symmetries in our languages\, and recove
 ring this symmetry restores the balance. I will present a style of program
 ming that emphasises the patterns of structures for user-defined data and 
 co-data types\, where induction and co-induction both blend together under
  the single umbrella of structural recursion.\nI will also discuss how to 
 prevent infinite loops and ensure termination (i.e.\, well-foundedness) by
  tracking the size of structures in types. The type-based approach to term
 ination gives a mechanism for encapsulating well-founded recursion princip
 les themselves as data and co-data types\, giving us first-class structure
 s for describing structural recursion.\n
LOCATION:Small Lecture Theatre\, Microsoft Research Ltd\, 21 Station Road\
 , Cambridge\, CB1 2FB
END:VEVENT
END:VCALENDAR