Welcome!

I am an Engineer in the Marelle team at Inria Sophia-Antipolis. I work on developing the Coq proof assistant and building a Consortium of academic and industrial users of Coq.

Previously, I was a postdoctoral researcher at Inria Paris-Rocquencourt, working under the supervision of Xavier Leroy in the Gallium research team. We were developing Coqonut, a formally verified JIT compiler for Coq.

Before that, I was a postdoctoral researcher at the University of Pennsylvania, working under the supervision of Benjamin C. Pierce on the SAFE project.

Before that, I was a PhD student working in the Marelle team at Inria Sophia-Antipolis, under the supervision of Yves Bertot and as part of the ForMath european project.

I defended my PhD thesis on November 20, 2013.

Research interests

My main research topics are formal proofs and program verification. More precisely, I am developing techniques to integrate advanced mathematical formalizations with efficient computing capabilities. I am a happy developer and user of the Coq proof assistant and the SSReflect extension.

I am also interested in :

  • Logic and type theory
  • Semantics of programming languages
  • Functional programming and compilation techniques