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 at the IRIF laboratory.

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.