Post-doctoral researcher in computer science, in the CLASH group at the University of Cambridge.
Before that, PhD student at Inria/University of Nantes in the Gallinette team, under the supervision of Nicolas Tabareau.
My main interests are dependent type theory and proofs assistants, in particular Rocq. I am also quite fond of everything revolving around bidirectional typing. One of the things I try to work towards is bridging the gap between the complex implementations of real-life proof assistants and their theoretic specifications, in particular in the framework of the MetaRocq project.
News
- 2025/07 – We have a new preprint on functorial types, continuing the work we presented at Types.
- 2025/07 – I presented my work on certifying conversion at FSCD, which won the best paper by a young researcher award!
- 2025/07 – Matthew Sirman's work for his master thesis, which I supervised and helped turn into a paper, has been published in the post-proceedings of Types '24.
- 2025/06 – Types was a blast! Arthur Adjedj presented our work on functorial types, and I was elected member of the conference's Steering Commitee.
- 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.
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.
