Arthur Charguéraud

According to our database, Arthur Charguéraud authored at least 37 papers between 2008 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Interactive Source-to-Source Optimizations Validated using Static Resource Analysis.

Guillaume Bertholon, Arthur Charguéraud, Thomas Koehler, Begatim Bytyqi, Damien Rouhling

Proceedings of the 13th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, 2024

2023

Review on <i>Functional Algorithms, Verified!</i>: <i>By Tobias Nipkow, Jasmin Blanchette, Manuel Eberl, Alejandro Gómez-Londoño, Peter Lammich, Christian Sternagel, Simon Wimmer, and Bohua Zhan</i> Freely downloadable: https://functional-algorithms-verified.org.

Arthur Charguéraud

Formal Aspects Comput., June, 2023

Omnisemantics: Smooth Handling of Nondeterminism.

Arthur Charguéraud, Adam Chlipala, Andres Erbsen, Samuel Gruetter

ACM Trans. Program. Lang. Syst., March, 2023

A High-Level Separation Logic for Heap Space under Garbage Collection.

Alexandre Moine, Arthur Charguéraud, François Pottier

Proc. ACM Program. Lang., January, 2023

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

2022

Specification and verification of a transient stack.

Alexandre Moine, Arthur Charguéraud, François Pottier

Proceedings of the CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17, 2022

2020

Separation logic for sequential programs (functional pearl).

Arthur Charguéraud

Proc. ACM Program. Lang., 2020

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

Provably and practically efficient granularity control.

Umut A. Acar, Vitaly Aksenov, Arthur Charguéraud, Mike Rainey

Proceedings of the 24th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2019

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm.

Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

GOSPEL - Providing OCaml with a Formal Specification Language.

Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço, Mário Pereira

Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

2018

MoSeL: a general, extensible modal framework for interactive proofs in separation logic.

Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer

Proc. ACM Program. Lang., 2018

JSExplain: A Double Debugger for JavaScript.

Arthur Charguéraud, Alan Schmitt, Thomas Wood

Proceedings of the Companion of the The Web Conference 2018 on The Web Conference 2018, 2018

Performance challenges in modular parallel programs.

Umut A. Acar, Vitaly Aksenov, Arthur Charguéraud, Mike Rainey

Proceedings of the 23rd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2018

Heartbeat scheduling: provable efficiency for nested parallelism.

Umut A. Acar, Arthur Charguéraud, Adrien Guatto, Mike Rainey, Filip Sieczkowski

Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Efficient Strict-Binning Particle-in-Cell Algorithm for Multi-core SIMD Processors.

Yann Barsamian, Arthur Charguéraud, Sever A. Hirstoaga, Michel Mehrenberger

Proceedings of the Euro-Par 2018: Parallel Processing, 2018

A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification.

Armaël Guéneau, Arthur Charguéraud, François Pottier

Proceedings of the Programming Languages and Systems, 2018

2017

Parallel Work Inflation, Memory Effects, and their Empirical Analysis.

Umut A. Acar, Arthur Charguéraud, Mike Rainey

CoRR, 2017

A Space and Bandwidth Efficient Multicore Algorithm for the Particle-in-Cell Method.

Yann Barsamian, Arthur Charguéraud, Alain Ketterlin

Proceedings of the Parallel Processing and Applied Mathematics, 2017

Temporary Read-Only Permissions for Separation Logic.

Arthur Charguéraud, François Pottier

Proceedings of the Programming Languages and Systems, 2017

2016

Oracle-guided scheduling for controlling granularity in implicitly parallel languages.

Umut A. Acar, Arthur Charguéraud, Mike Rainey

J. Funct. Program., 2016

Dag-calculus: a calculus for parallel computation.

Umut A. Acar, Arthur Charguéraud, Mike Rainey, Filip Sieczkowski

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

Higher-order representation predicates in separation logic.

Arthur Charguéraud

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

2015

A work-efficient algorithm for parallel unordered depth-first search.

Umut A. Acar, Arthur Charguéraud, Mike Rainey

Proceedings of the International Conference for High Performance Computing, 2015

Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation.

Arthur Charguéraud, François Pottier

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

2014

Improving Type Error Messages in OCaml.

Arthur Charguéraud

Proceedings of the Proceedings ML Family/OCaml Users and Developers workshops, 2014

A trusted mechanised JavaScript specification.

Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, Gareth Smith

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Theory and Practice of Chunked Sequences.

Umut A. Acar, Arthur Charguéraud, Mike Rainey

Proceedings of the Algorithms - ESA 2014, 2014

2013

Scheduling parallel programs by work stealing with private deques.

Umut A. Acar, Arthur Charguéraud, Mike Rainey

Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2013

Pretty-Big-Step Semantics.

Arthur Charguéraud

Proceedings of the Programming Languages and Systems, 2013

2012

The Locally Nameless Representation.

Arthur Charguéraud

J. Autom. Reason., 2012

2011

Oracle scheduling: controlling granularity in implicitly parallel languages.

Umut A. Acar, Arthur Charguéraud, Mike Rainey

Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2011

Characteristic formulae for the verification of imperative programs.

Arthur Charguéraud

Proceedings of the Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, 2011

2010

The Optimal Fixed Point Combinator.

Arthur Charguéraud

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Program verification through characteristic formulae.

Arthur Charguéraud

Proceedings of the Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, 2010

2008

Engineering formal metatheory.

Brian E. Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, Stephanie Weirich

Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

Functional translation of a calculus of capabilities.

Arthur Charguéraud, François Pottier

Proceedings of the Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, 2008