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.