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.