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.
I defended my PhD thesis on November 20, 2013.
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