I am a bit of an odd one at WITS: I have only written a single type-checker in my life, and that was for a not particularly complicated type system. But this was a fully verified type-checker! I will thus tell you a bit about my experience verifying dependent type-checkers, what I have learned by doing so both on the checkers themselves but also on the requirements for these efforts. And I hope I can even convince you that you might want to verify your own favourite implementation, and that it might be less crazy than you think…

BIO: Meven is a Postdoc at Inria and Université Paris Cité, and before that at the University of Cambridge and PhD student at Université de Nantes. Interested in anything having to do with proof assistants and dependent type theory, but particularly in the verification of proof assistant kernels and the meta-theory of dependent type systems.