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.
My research interests span from formal verification to multicore programming.
NEW — Course on Separation Logic for Sequential Programs
I wrote a master-level course on the Foundations of Separation Logic for sequential programs.
The course is written in the style of the Software Foundations series, and includes dozens of exercises.
It is suited for self-education.
More than 700,000 students participated in the contest in November 2019.
- 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.
Current students and postdocs:
- Damien Rouhling, Postdoc, started Oct 2019,
working on the OptiTrust project (see below).
Past PhD students:
- 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.
- OptiTrust ("Exploratory Action" funded by Inria, until October 2021), 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.
- ANR AJACS (until March 2019), led by Alan Schmitt,
- ERC DeepSea (until May 2018), led by Umut Acar,
on multicore programming and self-adjusting computations.
- 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.