BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A tour in (formalised) type theory - Meven Lennon-Bertrand (Univer
 sity of Cambridge)
DTSTART:20241107T170000Z
DTEND:20241107T180000Z
UID:TALK222379@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION: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*.\n\nI will try to explain the main properties we type theoris
 ts 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\, w
 hich aims to formalise the meta-theory of the Coq proof assistant inside i
 tself\, and Martin-Löf à la Coq\, a more recent exploration of proofs by
  logical relations.\n\nThe goal is to be accessible to users of these syst
 ems\, including (especially!) those that might not be very familiar with t
 heir foundations.\n\n\nSlides: https://www.meven.ac/category/talks.html
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR