title:Towards a certified proof assistant kernel – What it takes and what we have
abstract:|
TBA
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 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.
bio:|
Meven Lennon-Bertrand is a post-doctoral researcher in computer science, in the CLASH group at the University of Cambridge.
Previously he was a PhD student at Inria/University of Nantes in the Gallinette team, under the supervision of Nicolas Tabareau.
