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

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

The structures of induction and co-induction.

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.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

best pgdm colleges in bangalore One day Meeting (Cambridge Philosophical Society): Synthetic Biology - Molecular Bioengineering for the 21st Century Institute of Metabolic Science (IMS), Level 4 ATC, Seminar rooms 1,2 & 3

Other talks

Tea and Coffee Break Overview of treatment for non-small cell lung cancer Title and abstract tba Morning Tea and Coffee Title TBC Quantum optics with organic molecules
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity