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 the 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 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/09 – I'm starting a new job at IRIF and Inria.
- 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.bertrand@inria.fr.
Otherwise, I might be found at IRIF, in the Sophie Germain building, office 4058.
CV
Here is a print CV, most information can also be found directly by browsing this website.
