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-07 – I gave two talks at FLOC, one at the Rocqshop on porting a Rocq library, and one at ITP.
- 2026-07 – New pre-print, on using domain theory to prove meta-theoretic properties of MLTT without needing normalisation. Check it out!
- 2026/07 – Our work on (proof-relevant) interpolation and bidirectional typing, has appeared in the proceedings of ITP '26.
- 2026-06 – I gave an introduction to generalised algebraic theories at the Formal proof and sythetic mathematics school, slides are online.
- 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/09 – I'm starting a new job at IRIF and Inria.
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.
