I am a full-time researcher at Inria.

I am based in Strasbourg, in the Camus team, which is related to the ICPS team from the iCube lab.

My research interests span from formal verification to multicore programming.


NEWS


Selected papers:

Program verification
Multicore programming
Formal semantics

I design interactive challenges for the Concours Castor Informatique, french edition of the Bebras contest. It aims at raising children's interest for computer science.
More than 700,000 students participated in the contest in November 2019.

Responsabilities:

  • CADO 2020
    program committee member for the Special HPCS Session on Compiler Architecture, Design and Optimization.
  • POPL 2020
    program committee member for the Symposium on Principles of Programming Languages.
  • EJCP 2019
    co-organizer for the summer school École des Jeunes Chercheurs en Programmation.
  • OOPSLA 2019
    program committee member, papers getting published in the Proceedings of the ACM on Programming Languages (PACMPL).
  • ITP 2019
    program committee member for the International Conference on Interactive Theorem Proving
  • IFL 2018
    program committee member for the Symposium on Implementation and Application of Functional Languages.
  • VSTTE 2017
    program committee member for the Conference on Verified Software: Theories, Tools, and Experiments.
  • 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 2012
    PC member for the Coq workshop.

Recent invited talks:

  • ML Workshop 2020
    Verification of OCaml programs using CFML. Video.

Past PhD students and postdocs:

  • Damien Rouhling, Postdoc, Oct 2019 - August 2020,
    working on the OptiTrust project.
  • Armaël Guéneau, PhD student, co-advised with François Pottier, Sept 2017 - Dec 2019,
    working on the formal verification of asymptotic complexity properties.

Current funding:

  • OptiTrust ("Exploratory Action" funded by Inria, until summer 2022), funds a postdoc developing a framework for user-guided interactive source-to-source optimizations, with formal correctness guarantees.
  • ANR VOCAL (until October 2020), led by Jean-Christophe Filliâtre,
    on the formal verification of an OCaml library of data structures.

Past funding:

  • ANR AJACS (until March 2019), 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, 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 Paris (team Gallium), with François Pottier.