Abstract

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.