The structures of induction and co-induction.

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

• Paul Downen, University of Oregon.
• Thursday 17 September 2015, 15:00-16:00
• Small Lecture Theatre, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

 Please be aware that this event may be recorded. Microsoft will own the copyright of any recording and reserves the right to distribute it as required.

We know that induction and co-induction are two sides of the same 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 recovering this symmetry restores the balance. I will present a style of programming 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. I 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 termination gives a mechanism for encapsulating well-founded recursion principles themselves as data and co-data types, giving us first-class structures for describing structural recursion.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Small Lecture Theatre, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.