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.


BOOK


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, and more than 520,000 students in 2020 despite the pandemics.

Responsabilities:

  • POPL 2022
    program committee member for the Symposium on Principles of Programming Languages.
  • ASL 2022
    program committee member for the Internation Workshop on Advances in Separation Logic.
  • 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.

Current PhD student:

  • Alexandre Moine, PhD student, co-advised with François Pottier, Sept 2021 - Sept 2024,
    working on the formal verification of space bounds.

Current M2 intern:

  • Guillaume Bertholon, Febuary 2022 - July 2022,
    working on the formal verification of source-to-source transformations.

Past PhD student:

  • 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.
    Currently researcher at Inria Saclay.

Past postdocs:

  • Filip Sieczkowski, postdoc 2016-2017, co-advised with Umut Acar,
    working on the semantics of nested parallel computations.
    Currently assistant professor at the University of Wrocław.
  • Adrien Guatto, postdoc in 2017-2018, co-advised with Umut Acar,
    working the granularity control problem in parallel computations.
    Currently assistant professor at Université Paris-Diderot.
  • Damien Rouhling, Postdoc, 2019-2020,
    working on the OptiTrust project.
    Currently teacher in Classes Préparatoires.

Current funding:

  • OptiTrust ("Exploratory Action" funded by Inria, until August 2022), funds a postdoc developing a framework for user-guided interactive source-to-source optimizations.

Past funding:

  • ANR VOCAL (until March 2021), led by Jean-Christophe Filliâtre,
    on the formal verification of an OCaml library of data structures.
  • 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.