University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > A tour in (formalised) type theory

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

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

ℹ️ Information

A tour in (formalised) type theory

Download to your calendar using vCal

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:

Note that ex-directory lists are not shown.

Other lists

Lecture Theatre 2 and 3, Judge Business School (http://www.jbs.cam.ac.uk/aboutus/location.html) Ryle Seminar Room (930) Room W4.05 (Cambridge Judge Business School)

Other talks

Title to be confirmed Zooming in on the assembly of galaxies in the early Universe Director's Briefing Title TBC The rise of local cartography in Europe, 12th-14th century Group Work
 

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