Speaker: Meven LENNON-BERTRAND, University of Cambridge,mgapb2@cam.ac.uk
Tuesday 2024-12-17 14:00, Room to be announced
Abstract:
Proof assistant kernels are a natural target for program certification: they are critical, yet small and well-specified. Still, despite the maturity of type theory and software verification, we are yet to see a certified Agda, Coq or Lean. In my talk, I will give an overview of the landscape around this grand goal, more particularly of the interaction between certification and meta-theory, and present two complementary formalisation projects in that direction.
The core difficulty is that kernels rely on complex invariants, which in turn rest on significant properties of the type system. In essence, we cannot certify a kernel without first formalising the meta-theory of its type system. Historically, emphasis has been put on the *normalisation* property. I will explain why, in my view, other properties are more important, in particular the one called *injectivity of type constructors*.