Maître de conférences (~ assistant professor) at ENS Rennes. I do research within the Épicure team of INRIA and IRISA.
Before that, I was a postdoc in the Picube team at IRIF and at the University of Cambridge. I did my PhD in the Gallinette team, at INRIA and the University of Nantes.
Research
I am mainly interested in proofs assistants: I hope to make them better and safer by working on their logical foundation, dependent type theory. This involves trying to verify the complex implementations of today's proof assistants, and developing new type theoretic features to be (hopefully!) incorporated in the ones of tomorrow.
News
- 2026-09 – Simon Corbard is starting his PhD, co-supervised by Thibaut Benjamin and myself, with Sam van Gool as senior advisor.
- 2026-09 — I'm starting as a maître de conférences at ENS Rennes!
- 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.
Contact
The best way to reach me is by email, at meven.bertrand@inria.fr. My office is F211 at IRISA.
CV
Here is a pretty detailed analytic CV. Most information can be found directly on this website.
