A tour in (formalised) type theory

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

• Meven Lennon-Bertrand (University of Cambridge)
• Thursday 07 November 2024, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

In this talk, I will give a tour of (dependent) type theory, the logical formalism that underpins proofs assistants like Lean, Coq, Agda, or F*.

I will try to explain the main properties we type theorists care about for these systems, why, and how we can prove them. Most of this is based on two formalisation projects I have worked on: MetaCoq, which aims to formalise the meta-theory of the Coq proof assistant inside itself, and Martin-Löf à la Coq, a more recent exploration of proofs by logical relations.

The goal is to be accessible to users of these systems, including (especially!) those that might not be very familiar with their foundations.

Slides: https://www.meven.ac/category/talks.html

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.