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.


Selected papers:

Program verification
Multicore programming
  • Granularity control for nested parallelism: provably efficient granularity control (PPoPP'19).
  • Strict-binning PIC: efficient particle-in-cell simulations using chunk sequences (Euro-Par'18).
  • Heartbeat scheduling: provably-efficient scheduling for nested parallel programs (PLDI'18).
  • DAG calculus: a unifying model for describing high-level parallel constructs (ICFP'16).
  • Granularity control: using asymptotic complexity annotations to predict tasks size (JFP'16).
  • Parallel DFS: a work-efficient algorithm for parallel unordered depth-first search (SC'15).
  • Chunked sequences: an efficient sequence data structure for parallel algorithms (ESA'14).
  • Work stealing with private deques: scheduling without concurrent work queues (PPoPP'13).
Formal metatheory in Coq

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 600,000 students participated in the contest in November 2017.

Responsabilities:

  • POPL 2019: program committee member for the Symposium on Principles of Programming Languages.
  • OOPSLA 2019: program committee member, papers getting published in the Proceedings of the ACM on Programming Languages (PACMPL).
  • 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 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 March 2019), led by Alan Schmitt,
    on the formalization of JavaScript semantics and security properties.

Past funding:

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