What does it take to certify a conversion checker?

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

• Meven Lennon-Bertrand (University of Cambridge)
• Monday 03 February 2025, 13:00-14:00
• SS03, Computer Laboratory.

If you have a question about this talk, please contact Ariadne Si Suo .

The meat of a kernel for dependent types is a conversion checker, the procedure which compares types. Conversion checking is quite subtle, and certifying it does its job is no small feat, despite its value if we wish to trust the kernel, on which the whole proof assistant ecosystem rests.

In this context, the most prominent property is normalisation, which is necessary if we want to fully certify the conversion checker. However, there are contexts where normalisation is out of reach: it might be impossible to prove because of Gödel’s incompleteness theorem, or simply false! Yet, we would still like to know something about our conversion checker…

In this talk I propose to walk you through recent investigations I have done in the matter, all formalised in Rocq. In particular, I’ll try to convince you that maybe normalisation is not the only property we should care about, and in particular that injectivity properties deserve to be in the light.

This talk is part of the SANDWICH Seminar (Computer Laboratory) series.

This talk is included in these lists:

• SS03, Computer Laboratory
• tcw57’s list

Note that ex-directory lists are not shown.