I am a full-time researcher at Inria.

I am based in Strasbourg, in the Camus team, part of the ICPS team from the iCube lab.

I also work closely with the DeepSea project at Inria Paris.

My research interests span from programming languages to mechanized proofs.

Program verification
Multicore programming
Formal metatheory in Coq


  • 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.

Current funding:

  • ANR VOCAL (until October 2019), led by Jean-Christophe Filliâtre,
    on the formal verification of an OCaml library of data structures.
  • ANR AJACS (until June 2018), led by Alan Schmitt,
    on the formalization of JavaScript semantics and security properties.
  • ERC DeepSea (until May 2018), led by Umut Acar,
    on multicore programming and self-adjusting computations.

Short bio:

  • Since Sep. 2016: full-time researcher at Inria Nancy, working in Strasbourg (team Camus).
  • Oct. 2012 - Sep. 2016: full-time researcher at Inria Saclay (team Toccata).
  • Jan. 2011 - Sep. 2012: post-doc at the Max Planck Institute (MPI-SWS), with Umut Acar.
  • Sep. 2007 - Dec. 2010: PhD at Inria Rocquencourt (team Gallium), with François Pottier.