Arthur Charguéraud

Publication Activity (10 Years)

Years Active: 2008-2024
Publications (10 Years): 22

Top Topics

Consumer Price Index

Parallel Computation

Provably Correct

Garbage Collection

Top Venues

Proc. ACM Program. Lang.

Publications

Guillaume Bertholon, Arthur Charguéraud, Thomas Koehler, Begatim Bytyqi, Damien Rouhling
Interactive Source-to-Source Optimizations Validated using Static Resource Analysis. SOAP@PLDI (2024)
Arthur Charguéraud, Adam Chlipala, Andres Erbsen, Samuel Gruetter
Omnisemantics: Smooth Handling of Nondeterminism. ACM Trans. Program. Lang. Syst. 45 (1) (2023)
Alexandre Moine, Arthur Charguéraud, François Pottier
A High-Level Separation Logic for Heap Space under Garbage Collection. Proc. ACM Program. Lang. 7 (POPL) (2023)
Arthur Charguéraud
Freely downloadable: https://functional-algorithms-verified.org. Formal Aspects Comput. 35 (2) (2023)
Alexandre Moine, Arthur Charguéraud, François Pottier
Specification and verification of a transient stack. CPP (2022)
Arthur Charguéraud
Separation logic for sequential programs (functional pearl). Proc. ACM Program. Lang. 4 (ICFP) (2020)
Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço, Mário Pereira
GOSPEL - Providing OCaml with a Formal Specification Language. FM (2019)
Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. ITP (2019)
Arthur Charguéraud, François Pottier
Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits. J. Autom. Reason. 62 (3) (2019)
Umut A. Acar, Vitaly Aksenov, Arthur Charguéraud, Mike Rainey
Provably and practically efficient granularity control. PPoPP (2019)
Yann Barsamian, Arthur Charguéraud, Sever A. Hirstoaga, Michel Mehrenberger
Efficient Strict-Binning Particle-in-Cell Algorithm for Multi-core SIMD Processors. Euro-Par (2018)
Armaël Guéneau, Arthur Charguéraud, François Pottier
A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification. ESOP (2018)
Umut A. Acar, Arthur Charguéraud, Adrien Guatto, Mike Rainey, Filip Sieczkowski
Heartbeat scheduling: provable efficiency for nested parallelism. PLDI (2018)
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
MoSeL: a general, extensible modal framework for interactive proofs in separation logic. Proc. ACM Program. Lang. 2 (ICFP) (2018)
Arthur Charguéraud, Alan Schmitt, Thomas Wood
JSExplain: A Double Debugger for JavaScript. WWW (Companion Volume) (2018)
Umut A. Acar, Vitaly Aksenov, Arthur Charguéraud, Mike Rainey
Performance challenges in modular parallel programs. PPOPP (2018)
Umut A. Acar, Arthur Charguéraud, Mike Rainey
Parallel Work Inflation, Memory Effects, and their Empirical Analysis. CoRR (2017)
Yann Barsamian, Arthur Charguéraud, Alain Ketterlin
A Space and Bandwidth Efficient Multicore Algorithm for the Particle-in-Cell Method. PPAM (1) (2017)
Arthur Charguéraud, François Pottier
Temporary Read-Only Permissions for Separation Logic. ESOP (2017)
Umut A. Acar, Arthur Charguéraud, Mike Rainey
Oracle-guided scheduling for controlling granularity in implicitly parallel languages. J. Funct. Program. 26 (2016)
Arthur Charguéraud
Higher-order representation predicates in separation logic. CPP (2016)
Umut A. Acar, Arthur Charguéraud, Mike Rainey, Filip Sieczkowski
Dag-calculus: a calculus for parallel computation. ICFP (2016)
Umut A. Acar, Arthur Charguéraud, Mike Rainey
A work-efficient algorithm for parallel unordered depth-first search. SC (2015)
Arthur Charguéraud, François Pottier
Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. ITP (2015)
Umut A. Acar, Arthur Charguéraud, Mike Rainey
Theory and Practice of Chunked Sequences. ESA (2014)
Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, Gareth Smith
A trusted mechanised JavaScript specification. POPL (2014)
Arthur Charguéraud
Improving Type Error Messages in OCaml. ML/OCaml (2014)
Arthur Charguéraud
Pretty-Big-Step Semantics. ESOP (2013)
Umut A. Acar, Arthur Charguéraud, Mike Rainey
Scheduling parallel programs by work stealing with private deques. PPOPP (2013)
Arthur Charguéraud
The Locally Nameless Representation. J. Autom. Reason. 49 (3) (2012)
Arthur Charguéraud
Characteristic formulae for the verification of imperative programs. ICFP (2011)
Umut A. Acar, Arthur Charguéraud, Mike Rainey
Oracle scheduling: controlling granularity in implicitly parallel languages. OOPSLA (2011)
Arthur Charguéraud
Program verification through characteristic formulae. ICFP (2010)
Arthur Charguéraud
The Optimal Fixed Point Combinator. ITP (2010)
Brian E. Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, Stephanie Weirich
Engineering formal metatheory. POPL (2008)
Arthur Charguéraud, François Pottier
Functional translation of a calculus of capabilities. ICFP (2008)