Arthur Charguéraud
Arthur Charguéraud
Verified email at
Cited by
Cited by
Engineering formal metatheory
B Aydemir, A Charguéraud, BC Pierce, R Pollack, S Weirich
Acm sigplan notices 43 (1), 3-15, 2008
The locally nameless representation
A Charguéraud
Journal of automated reasoning 49, 363-408, 2012
Scheduling parallel programs by work stealing with private deques
UA Acar, A Charguéraud, M Rainey
Proceedings of the 18th ACM SIGPLAN symposium on Principles and practice of …, 2013
A trusted mechanised JavaScript specification
M Bodin, A Charguéraud, D Filaretti, P Gardner, S Maffeis, ...
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of …, 2014
Characteristic formulae for the verification of imperative programs
A Charguéraud
Proceedings of the 16th ACM SIGPLAN international conference on Functional …, 2011
MoSeL: A general, extensible modal framework for interactive proofs in separation logic
R Krebbers, JH Jourdan, R Jung, J Tassarotti, JO Kaiser, A Timany, ...
Proceedings of the ACM on Programming Languages 2 (ICFP), 1-30, 2018
Pretty-big-step semantics
A Charguéraud
European Symposium on Programming, 41-60, 2013
Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
A Charguéraud, F Pottier
Journal of Automated Reasoning 62 (3), 331-365, 2019
Functional translation of a calculus of capabilities
A Charguéraud, F Pottier
Proceedings of the 13th ACM SIGPLAN international conference on Functional …, 2008
Program verification through characteristic formulae
A Charguéraud
Proceedings of the 15th ACM SIGPLAN International Conference on Functional …, 2010
A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification
A Guéneau, A Charguéraud, F Pottier
European Symposium on Programming, 533-560, 2018
Separation logic for sequential programs (functional pearl)
A Charguéraud
Proceedings of the ACM on Programming Languages 4 (ICFP), 1-34, 2020
Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
A Charguéraud, F Pottier
International Conference on Interactive Theorem Proving, 137-153, 2015
Oracle scheduling: Controlling granularity in implicitly parallel languages
UA Acar, A Charguéraud, M Rainey
ACM Sigplan Notices 46 (10), 499-518, 2011
Formal proof and analysis of an incremental cycle detection algorithm
A Guéneau, JH Jourdan, A Charguéraud, F Pottier
Interactive Theorem Proving, 2019
Characteristic formulae for mechanized program verification
A Charguéraud
PhD thesis, Université Paris 7, 2010
Temporary read-only permissions for separation logic
A Charguéraud, F Pottier
Programming Languages and Systems: 26th European Symposium on Programming …, 2017
Heartbeat scheduling: Provable efficiency for nested parallelism
UA Acar, A Charguéraud, A Guatto, M Rainey, F Sieczkowski
Proceedings of the 39th ACM SIGPLAN Conference on Programming Language …, 2018
A work-efficient algorithm for parallel unordered depth-first search
UA Acar, A Charguéraud, M Rainey
Proceedings of the International Conference for High Performance Computing …, 2015
GOSPEL—providing OCaml with a formal specification language
A Charguéraud, JC Filliâtre, C Lourenço, M Pereira
Formal Methods–The Next 30 Years: Third World Congress, FM 2019, Porto …, 2019
The system can't perform the operation now. Try again later.
Articles 1–20