I am a full-time researcher at Inria.

I am based in Saclay, in the Toccata team, also part of the VALS team.

I am also involved in the DeepSea project at Inria Paris.

My research interests span from programming languages to mechanized proofs.

Program verification
Formal metatheory in Coq
Multicore programming
Libraries for the Coq proof assistant


  • CoqPL 2016: PC chair for the 2nd International Workshop on Coq for Programming Languages.
  • ESOP 2016: PC member for the 25th European Symposium on Programming.
  • POPL 2015: member of the external review committee for the 42nd Symposium on Principles of Programming Languages.
  • Coq Workshop 2012: PC member for the 4th International Workshop on Coq.