Arthur Charguéraud's home page

I work as a senior 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 interactive program verification to high-performance programming.

BOOK

Separation Logic Foundations is now published as volume 6 of the Software Foundations series, edited by Benjamin C. Pierce.

If you prefer reading LaTeX over Coq, you may be interested in the companion course notes.

More advanced material is covered in my habilitation manuscript.

Selected papers:

Program verification

Habilitation manuscript: a modern eye on separation logic for sequential programs (2023).
Separation logic with space credits: formal space bounds in the presence of a GC (POPL'22).
Verification of a transient data structure: efficience and persistence, formalized (CPP'22).
This paper received a distinguished paper award.
Separation logic for sequential programs: a tutorial covering recent innovations (ICFP'20).
A surface language for Separation logic: more concise specifications for ML programs (FM'19).
Verification of an incremental cycle detection algorithm: a case study with formal big-O (ITP'19).
Separation logic tactic framework: the MoSel extensible modal framework (ICFP'18).
Separation logic with big-O notation: verification of asymptotic complexity claims (ESOP'18).
Separation logic with temporary read-only permissions: simpler specifications (ESOP'17).
Separation logic with time credits: amortized asymptotic time bounds (ITP'15, JAR'17).
Higher-order representation predicates: specification of polymorphic data structures (CPP'16).
Characteristic formulae: interactive verification of imperative ML programs (ICFP'11).

Multicore programming

Granularity control using complexity functions: robust and efficient granularity control (PPoPP'19).
This paper received a SIGPLAN Research Highlight.
Heartbeat scheduling: provably-efficient scheduling for nested parallel programs (PLDI'18).
Strict-binning PIC: efficient particle-in-cell simulations using chunk sequences (Euro-Par'18).
DAG calculus: a unifying model for describing high-level parallel constructs (ICFP'16).
Granularity control: asymptotic complexity annotations to predict tasks size (OOPSLA'11, 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 semantics

Omnisemantics: smooth handling of nondeterminism (TOPLAS'23).
JSExplain: a double debugger for JavaScript (WepProg'18).
Formalization of JavaScript: pretty-big-step semantics and executable interpreter (POPL'16).
Pretty-big-step semantics: overcoming the limitations of the big-step semantics (ESOP'13).
The optimal fixed foint combinator: nontrival partial recursive functions in classical logic (ITP'10).
Locally nameless with cofinite quantification: proofs with variable bindings (POPL'08, JAR'09).

Program optimization

OptiTrust: an interactive framework for source-to-source transformations (Draft, 2022).

See my complete list of publications.

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.

700,000 students participated in the contest in December 2023.

Responsabilities:

ICFP 2024
program committee member for the International Conference on Functional Programming.
CPP 2024
program committee member for the International Conference on Certified Programs and Proofs.
CoqPL 2024
program committee member for the International Workshop on Coq for Programming Languages.
JFLA 2024
program committee member for the Journées Francophones des Langages Applicatifs.
POPL 2022
program committee member for the Symposium on Principles of Programming Languages.
ASL 2022
program committee member for the International 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
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
PC chair for the 2nd International Workshop on Coq for Programming Languages.
ESOP 2016
PC member for the European Symposium on Programming.
POPL 2015
member of the external review committee for the Symposium on Principles of Programming Languages.
Coq 2012
PC member for the Coq workshop.

Selected invited talks:

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

Current PhD students:

Alexandre Moine, PhD student, co-advised with François Pottier, Sept 2021 - Sept 2024,
working on the formal verification of space bounds.
Guillaume Bertholon, PhD student, Sept 2022 - Sept 2025,
working on the formal verification of source-to-source transformations.

Current postdoc:

Thomas Koehler, postdoc, Jan 2023 - Dec 2024,
working on the OptiTrust project.

Past PhD student:

Armaël Guéneau, PhD student, co-advised with François Pottier, Sept 2016 - 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 Heriot-Watt University.
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:

ANR OptiTrust (Oct. 2022 - Sept. 2026), led by Arthur Charguéraud,
on an interactive source-to-source transformation framework with formal guarantees.
ANR GOSPEL (Jan. 2023 - Dec. 2026), led by François Pottier,
on the design of a formal specification language for OCaml.

Past funding:

Inria "Exploratory Action" (Sept. 2019 - Aug. 2022), led by Arthur Charguéraud,
development of the OptiTrust framework for user-guided source-to-source optimizations.
ANR VOCAL (Oct. 2015 - March 2021), led by Jean-Christophe Filliâtre,
on the formal verification of an OCaml library of data structures.
ANR AJACS (Dec. 2014 - March 2019), led by Alan Schmitt,
on the formalization of JavaScript semantics and security properties.
ERC DeepSea (June 2013 - May 2018), led by Umut Acar,
on multicore programming and self-adjusting computations.

Short bio:

Since Oct. 2024: full-time senior researcher at Inria, working in Strasbourg (team Camus).
Sep. 2016 - Sep. 2024: 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.