Post-doctoral researcher in computer science, in the CLASH group at the University of Cambrige.
Before that, PhD student at Inria/University of Nantes in the Gallinette team, under the supervision of Nicolas Tabareau.
My main interests are type theory and proofs assistants, in particular Coq. I am also quite fond of everything revolving around bidirectional typing. One of the things I try and work towards is bridging the gap between complex, real-life implementations of proof assistants and their theoretic specifications, in particular in the framework of the MetaCoq project.
News
- 2025/02 – A new preprint is out, on how to certify conversion-checking algorithms.
- 2025/01 – Our paper on MetaCoq has appeared at the Journal of the ACM.
- 2024/12 – I will be in the PC of ITP '25.
- 2024/10 – I will be lecturing two courses this year, Denotational Semantics and Proof Assistants.
- 2024/09 – A new version of our MetaCoq paper is out.
Contact
The best way to reach me is by email, at Meven.Lennon-Bertrand[at]cl.cam.ac.uk.
Otherwise, I might be found at the Computer Lab's William Gates Building, office FS18.
CV
Here is a print CV, most information can also be found directly by browsing this website.
