Thursday 14 December 2023, 15:00, room 1Z76 (or online): Towards a certified proof assistant kernel — What it takes and what we have, Meven Lennon-Bertrand (University of Cambridge).

Proof assistant kernels are a natural target for program certification: they are small, critical, and well-specified. Still, despite the maturity of the field of software certification, we are yet to see a certified Agda, Coq or Lean. In this talk, I will try and explain why this is not such an easy task, and present you two complementary projects going in that direction. The first, MetaCoq, is a large scale project, broadly aiming at giving tools to manipulate Coq terms and derivations inside of Coq, in particular developing an important body of formalized proofs around Coq's typing. The second is a more recent endeavour, aimed at tackling the mother of all properties: normalisation.