Arthur Charguéraud

38 papers A* 3A 10B 9Journal 10Unranked 5

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