skip to content

Department of Computer Science and Technology

Date: 
Thursday, 7 November, 2024 - 17:00 to 18:00
Speaker: 
Meven Lennon-Bertrand (University of Cambridge)
Venue: 
MR14 Centre for Mathematical Sciences

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.

=== Hybrid talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1

Meeting ID: 871 4336 5195

Passcode: 541180

Seminar series: 
Formalisation of mathematics with interactive theorem provers

Upcoming seminars