en ¦ fr


Post-doctoral researcher in computer science, in the CLASH group at the University of Cambrige.

Before that, PhD student in the Inria/University of Nantes Gallinette team, under the supervision of Nicolas Tabareau. Even before that, student in the computer science department of the ENS de Lyon, and for a year in the Mathematical Foundation of Computer Science master of the Radboud University Nijmegen.

I work mainly around proof assistants, chiefly those based on type theory, and in particular Coq. I am also fond of type theory in general, and especially of bidirectional typing. I mainly try to bridge the gap between complex, real-life implementations of proof assistants and their theoretic specifications, in particular in the framework of the MetaCoq project.


The best way to reach me is by email, at mgapb2[at]cam.ac.uk.

Otherwise, I might be found at the Computer Lab's William Gates Building.


Here is a print CV, most information can also be found directly by browsing this website.

Under Creative Commons CC0 License, source on github. Built using Pelican. Theme adapted from pelican-svbhack by Giulio Fidente.