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.
More than 700,000 students participated in the contest in November 2019, and more than 520,000 students in 2020 despite the pandemics.
- 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.
- Alexandre Moine, M2 Intern, 2021, co-advised with François Pottier
working on the verification of a transient data structure.
Past PhD students and postdocs:
- Damien Rouhling, Postdoc, Oct 2019 - August 2020,
working on the OptiTrust project. Now teacher in Prépa.
- 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. Now researcher at Inria.
- OptiTrust ("Exploratory Action" funded by Inria, until August 2022), funds a postdoc developing a framework for user-guided interactive source-to-source optimizations, with formal correctness guarantees.
- 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,
- 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.