BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:What does it take to certify a conversion checker? - Meven Lennon-
 Bertrand (University of Cambridge)
DTSTART:20250203T130000Z
DTEND:20250203T140000Z
UID:TALK226360@talks.cam.ac.uk
CONTACT:Ariadne Si Suo
DESCRIPTION:The meat of a kernel for dependent types is a conversion check
 er\, the procedure which compares types. Conversion checking is quite subt
 le\, and certifying it does its job is no small feat\, despite its value i
 f we wish to trust the kernel\, on which the whole proof assistant ecosyst
 em rests.\n\nIn this context\, the most prominent property is normalisatio
 n\, which is necessary if we want to fully certify the conversion checker.
  However\, there are contexts where normalisation is out of reach: it migh
 t be impossible to prove because of Gödel's incompleteness theorem\, or s
 imply false! Yet\, we would still like to know _something_ about our conve
 rsion checker…\n\nIn this talk I propose to walk you through recent inve
 stigations I have done in the matter\, all formalised in Rocq. In particul
 ar\, I'll try to convince you that maybe normalisation is not the only pro
 perty we should care about\, and in particular that _injectivity_ properti
 es deserve to be in the light.
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR