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 went to do postdoctoral studies at Harvard, working in the Ynot group. I am now a researcher at INRIA Paris working in the pi.r2 team.

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.