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


  • HaTT 2016: program committee member for the International Workshop on Hammers for Type Theories.
  • ICFP 2016: external review committee member for the International Conference on Functional Programming.
  • ML 2016: PC member for the ML family workshop.
  • 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.