Post-doctoral researcher in computer science at Inria and IRIF.
Before that, postdoc at the University of Cambridge, and even before that PhD student in Inria team Gallinette at the University of Nantes.
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 work towards is bridging the gap between the complex implementations of real-life proof assistants and their theoretic specifications.
News
- 2026-06 – I'll be talking at the Formal proof and sythetic mathematics school.
- 2026/03 – Our preprint with Alexis Saurin, on (proof-relevant) interpolation and bidirectional typing, has been accepted at ITP '26. See you in Lisbon!
- 2026/01 – I gave two talks at POPL '26: I presented AdapTT in the main track, and gave an invited talk at WITS. Slides for both are online.
- 2025/11 – Our paper on adapters has just been accepted for POPL '26.
- 2025/09 – I'm starting a new job at IRIF and Inria.
- 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.
Contact
The best way to reach me is by email, at meven.bertrand@inria.fr.
Otherwise, I might be found at IRIF, in the Sophie Germain building, office 4058.
CV
Here is a painfully detailed analytic CV. Most information can be found directly on this website.
