International journals
Oracle-Guided Scheduling for Controlling Granularity in Implicitly Parallel Languages
Umut A. Acar, Arthur Charguéraud and Mike Rainey
JFP: Journal of Functional Programming, December 2016
Improving Type Error Messages in OCaml
Arthur Charguéraud
ETPCS: Post-proceedings of the ML/OCaml 2014 workshops, November 2015
The Locally Nameless Representation
Arthur Charguéraud
JAR: Journal of Automated Reasoning, May 2011
International conferences
Temporary Read-Only Permissions for Separation Logic
Arthur Charguéraud and François Pottier
ESOP: European Symposium on Programming, April 2017
Dag-Calculus: A Calculus for Parallel Computation
Umut A. Acar, Arthur Chargueraud, Mike Rainey, and Filip Sieczkowski
ICFP: International Conference on Functional Programming, September 2016
Higher-order Representation Predicates in Separation Logic
Arthur Charguéraud
CPP: Certified Programs and Proofs, January 2016
Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
Arthur Charguéraud and François Pottier
ITP: International Conference on Interactive Theorem Proving, August 2015
A Work-Efficient Algorithm for Parallel Unordered Depth-First Search
Umut A. Acar, Arthur Chargueraud and Mike Rainey
SC: ACM/IEEE Conference on High Performance Computing, November 2015
Theory and Practice of Chunked Sequences
Umut A. Acar, Arthur Charguéraud and Mike Rainey
ESA: European Symposium on Algorithms, September 2014
A Trusted Mechanised JavaScript Specification
Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt and Gareth Smith
POPL: Symposium on Principles of Programming Languages, January 2014
Scheduling Parallel Programs by Work Stealing with Private Deques
Umut A. Acar, Arthur Charguéraud and Mike Rainey
PPOPP: Symposium on Principles and Practice of Parallel Programming, Febuary 2013
Pretty-Big-Step Semantics
Arthur Charguéraud
ESOP: European Symposium on Programming, March 2013
Oracle Scheduling: Controlling Granularity in Implicitly Parallel Languages
Umut A. Acar, Arthur Charguéraud and Mike Rainey
OOPSLA, October 2011
Characteristic Formulae for the Verification of Imperative Programs
Arthur Charguéraud
ICFP: International Conference on Functional Programming, September 2011
The Optimal Fixed Point Combinator
Arthur Charguéraud
ITP: International Conference on Interactive Theorem Proving, July 2010
Program Verification Through Characteristic Formulae
Arthur Charguéraud
ICFP: International Conference on Functional Programming, September 2010
Functional Translation of a Calculus of Capabilities
Arthur Charguéraud and François Pottier
ICFP: International Conference on Functional Programming, September 2008
Engineering Formal Metatheory
Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack and Stephanie Weirich
POPL: Symposium on Principles of Programming Languages, January 2008
International workshops
Efficient Primitives for Creating and Scheduling Parallel Computations
Umut A. Acar, Arthur Charguéraud and Mike Rainey
DAMP: Workshop on Declarative Aspects and Applications of Multicore Programming, January 2012
Reports
Data Structures and Algorithms for Robust and Fast Parallel Graph Search
Umut A. Acar, Arthur Charguéraud and Mike Rainey
Inria Technical Report, September 2014
Atomic Read-Modify-Write Operations are Unnecessary for Shared-Memory Work Stealing
Umut A. Acar, Arthur Charguéraud, Stefan Muller and Mike Rainey
Inria Technical Report, September 2013
Characteristic Formulae for the Verification of Imperative Programs
Arthur Charguéraud
Report, journal version of the ICFP'11 paper, October 2012
Characteristic Formulae for Mechanized Program Verification
Arthur Charguéraud
PhD thesis, December 2010
Proof Pearl: A Constructive Fixed Point Combinator for Recursive Functions
Arthur Charguéraud
Report, March 2009
Interactive Verification of Call-by-Value Functional Programs Through a Deep Embedding
Arthur Charguéraud
Report, March 2009