I was a PhD student at the university of Paris XI in the LRI laboratory, working in the Démons team under supervision of Christine Paulin-Mohring. I have defended my thesis on An environment for programming with dependent types and I am now a postdoctoral fellow at Harvard, working in the Ynot group. I will move to INRIA Paris to work as a full-time researcher in the pi.r2 team in October.

My research interests spans logic and computer science, from the study of type theory and design of dependently-typed functional programming languages to interactive and automated reasoning. I am interested in the implementation and the use of proof assistants for verifying software and constructing mechanically-verified, formal proofs.

I am one of the main developers of the Coq proof assistant and have made significant developments in the system using the novel tools I added to it (notably Program and Type Classes). I've been working recently on a dependent pattern-matching compiler and a new rewriting tactic. I am part of the GoNative project providing verifiable guarantees for native binary code execution.