Functional translation of a calculus of capabilities. - Arthur Charguéraud; François Pottier (ICFP, 2008)

Engineering formal metatheory. - Brian E. Aydemir; Arthur Charguéraud; Benjamin C. Pierce; Randy Pollack; Stephanie Weirich (POPL, 2008)

Program verification through characteristic formulae. - Arthur Charguéraud (ICFP, 2010)

The Optimal Fixed Point Combinator. - Arthur Charguéraud (ITP, 2010)

Characteristic formulae for the verification of imperative programs. - Arthur Charguéraud (ICFP, 2011)

Oracle scheduling: controlling granularity in implicitly parallel languages. - Umut A. Acar; Arthur Charguéraud; Mike Rainey (OOPSLA, 2011)

The Locally Nameless Representation. - Arthur Charguéraud (J. Autom. Reason., 2012)

Pretty-Big-Step Semantics. - Arthur Charguéraud (ESOP, 2013)

Scheduling parallel programs by work stealing with private deques. - Umut A. Acar; Arthur Charguéraud; Mike Rainey (PPoPP, 2013)

Theory and Practice of Chunked Sequences. - Umut A. Acar; Arthur Charguéraud; Mike Rainey (ESA, 2014)

A trusted mechanised JavaScript specification. - Martin Bodin; Arthur Charguéraud; Daniele Filaretti; Philippa Gardner; Sergio Maffeis; Daiva Naudziuniene; Alan Schmitt; Gareth Smith (POPL, 2014)

Improving Type Error Messages in OCaml. - Arthur Charguéraud (ML/OCaml, 2014)

Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. - Arthur Charguéraud; François Pottier (ITP, 2015)

A work-efficient algorithm for parallel unordered depth-first search. - Umut A. Acar; Arthur Charguéraud; Mike Rainey (SC, 2015)

Higher-order representation predicates in separation logic. - Arthur Charguéraud (CPP, 2016)

Dag-calculus: a calculus for parallel computation. - Umut A. Acar; Arthur Charguéraud; Mike Rainey; Filip Sieczkowski (ICFP, 2016)

Oracle-guided scheduling for controlling granularity in implicitly parallel languages. - Umut A. Acar; Arthur Charguéraud; Mike Rainey (J. Funct. Program., 2016)

Temporary Read-Only Permissions for Separation Logic. - Arthur Charguéraud; François Pottier (ESOP, 2017)

A Space and Bandwidth Efficient Multicore Algorithm for the Particle-in-Cell Method. - Yann Barsamian; Arthur Charguéraud; Alain Ketterlin (PPAM (1), 2017)

Parallel Work Inflation, Memory Effects, and their Empirical Analysis. - Umut A. Acar; Arthur Charguéraud; Mike Rainey (CoRR, 2017)

A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification. - Armaël Guéneau; Arthur Charguéraud; François Pottier (ESOP, 2018)

Efficient Strict-Binning Particle-in-Cell Algorithm for Multi-core SIMD Processors. - Yann Barsamian; Arthur Charguéraud; Sever A. Hirstoaga; Michel Mehrenberger (Euro-Par, 2018)

Heartbeat scheduling: provable efficiency for nested parallelism. - Umut A. Acar; Arthur Charguéraud; Adrien Guatto; Mike Rainey; Filip Sieczkowski (PLDI, 2018)

Performance challenges in modular parallel programs. - Umut A. Acar; Vitaly Aksenov; Arthur Charguéraud; Mike Rainey (PPoPP, 2018)

JSExplain: A Double Debugger for JavaScript. - Arthur Charguéraud; Alan Schmitt; Thomas Wood 001 (WWW (Companion Volume), 2018)

MoSeL: a general, extensible modal framework for interactive proofs in separation logic. - Robbert Krebbers; Jacques-Henri Jourdan; Ralf Jung 002; Joseph Tassarotti; Jan-Oliver Kaiser; Amin Timany; Arthur Charguéraud; Derek Dreyer (Proc. ACM Program. Lang., 2018)

GOSPEL - Providing OCaml with a Formal Specification Language. - Arthur Charguéraud; Jean-Christophe Filliâtre; Cláudio Lourenço; Mário Pereira (FM, 2019)

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. - Armaël Guéneau; Jacques-Henri Jourdan; Arthur Charguéraud; François Pottier (ITP, 2019)

Provably and practically efficient granularity control. - Umut A. Acar; Vitaly Aksenov; Arthur Charguéraud; Mike Rainey (PPoPP, 2019)

Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits. - Arthur Charguéraud; François Pottier (J. Autom. Reason., 2019)

Separation logic for sequential programs (functional pearl). - Arthur Charguéraud (Proc. ACM Program. Lang., 2020)

Specification and verification of a transient stack. - Alexandre Moine 001; Arthur Charguéraud; François Pottier (CPP, 2022)

A Modern Eye on Separation Logic for Sequential Programs. (Un nouveau regard sur la Logique de Séparation pour les programmes séquentiels). - Arthur Charguéraud (2023)

A High-Level Separation Logic for Heap Space under Garbage Collection. - Alexandre Moine 001; Arthur Charguéraud; François Pottier (Proc. ACM Program. Lang., 2023)

Omnisemantics: Smooth Handling of Nondeterminism. - Arthur Charguéraud; Adam Chlipala; Andres Erbsen; Samuel Gruetter (ACM Trans. Program. Lang. Syst., 2023)

Review on Functional Algorithms, Verified!: By Tobias Nipkow, Jasmin Blanchette, Manuel Eberl, Alejandro Gómez-Londoño, Peter Lammich, Christian Sternagel, Simon Wimmer, and Bohua Zhan Freely downloadable: https://functional-algorithms-verified.org. - Arthur Charguéraud (Formal Aspects Comput., 2023)

Interactive Source-to-Source Optimizations Validated using Static Resource Analysis. - Guillaume Bertholon; Arthur Charguéraud; Thomas Koehler 005; Begatim Bytyqi; Damien Rouhling (SOAP@PLDI, 2024)

Will It Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection. - Alexandre Moine 001; Arthur Charguéraud; François Pottier (ACM Trans. Program. Lang. Syst., 2025)