University of Cambridge > > Microsoft Research Cambridge, public talks > The structures of induction and co-induction.

The structures of induction and co-induction.

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2022, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity