| 2022 | CPP | Specification and verification of a transient stack. | Alexandre Moine, Arthur Charguraud, Franois Pottier |
| 2019 | FM | GOSPEL - Providing OCaml with a Formal Specification Language. | Arthur Charguraud, Jean-Christophe Fillitre, Cludio Loureno, Mrio Pereira |
| 2019 | ITP | Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. | Armal Guneau, Jacques-Henri Jourdan, Arthur Charguraud, Franois Pottier |
| 2019 | PPoPP | Provably and practically efficient granularity control. | Umut A. Acar, Vitaly Aksenov, Arthur Charguraud, Mike Rainey |
| 2018 | ESOP | A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification. | Armal Guneau, Arthur Charguraud, Franois Pottier |
| 2018 | EuroPar | Efficient Strict-Binning Particle-in-Cell Algorithm for Multi-core SIMD Processors. | Yann Barsamian, Arthur Charguraud, Sever A. Hirstoaga, Michel Mehrenberger |
| 2018 | PLDI | Heartbeat scheduling: provable efficiency for nested parallelism. | Umut A. Acar, Arthur Charguraud, Adrien Guatto, Mike Rainey, Filip Sieczkowski |
| 2018 | PPoPP | Performance challenges in modular parallel programs. | Umut A. Acar, Vitaly Aksenov, Arthur Charguraud, Mike Rainey |
| 2018 | WWW | JSExplain: A Double Debugger for JavaScript. | Arthur Charguraud, Alan Schmitt, Thomas Wood |
| 2017 | ESOP | Temporary Read-Only Permissions for Separation Logic. | Arthur Charguraud, Franois Pottier |
| 2017 | PPAM | A Space and Bandwidth Efficient Multicore Algorithm for the Particle-in-Cell Method. | Yann Barsamian, Arthur Charguraud, Alain Ketterlin |
| 2016 | CPP | Higher-order representation predicates in separation logic. | Arthur Charguraud |
| 2016 | ICFP | Dag-calculus: a calculus for parallel computation. | Umut A. Acar, Arthur Charguraud, Mike Rainey, Filip Sieczkowski |
| 2015 | ITP | Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. | Arthur Charguraud, Franois Pottier |
| 2015 | SC | A work-efficient algorithm for parallel unordered depth-first search. | Umut A. Acar, Arthur Charguraud, Mike Rainey |
| 2014 | ESA | Theory and Practice of Chunked Sequences. | Umut A. Acar, Arthur Charguraud, Mike Rainey |
| 2014 | POPL | A trusted mechanised JavaScript specification. | Martin Bodin, Arthur Charguraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, Gareth Smith |
| 2013 | ESOP | Pretty-Big-Step Semantics. | Arthur Charguraud |
| 2013 | PPoPP | Scheduling parallel programs by work stealing with private deques. | Umut A. Acar, Arthur Charguraud, Mike Rainey |
| 2011 | ICFP | Characteristic formulae for the verification of imperative programs. | Arthur Charguraud |
| 2011 | OOPSLA | Oracle scheduling: controlling granularity in implicitly parallel languages. | Umut A. Acar, Arthur Charguraud, Mike Rainey |
| 2010 | ICFP | Program verification through characteristic formulae. | Arthur Charguraud |
| 2010 | ITP | The Optimal Fixed Point Combinator. | Arthur Charguraud |
| 2008 | ICFP | Functional translation of a calculus of capabilities. | Arthur Charguraud, Franois Pottier |
| 2008 | POPL | Engineering formal metatheory. | Brian E. Aydemir, Arthur Charguraud, Benjamin C. Pierce, Randy Pollack, Stephanie Weirich |