Follow
Arthur Charguéraud
Arthur Charguéraud
Verified email at inria.fr
Title
Cited by
Cited by
Year
Engineering formal metatheory
B Aydemir, A Charguéraud, BC Pierce, R Pollack, S Weirich
Acm sigplan notices 43 (1), 3-15, 2008
3072008
The locally nameless representation
A Charguéraud
Journal of automated reasoning 49, 363-408, 2012
2352012
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
1762014
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
1742013
Characteristic formulae for the verification of imperative programs
A Charguéraud
Proceedings of the 16th ACM SIGPLAN international conference on Functional …, 2011
1442011
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
1092018
Pretty-big-step semantics
A Charguéraud
European Symposium on Programming, 41-60, 2013
1022013
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
872019
Functional translation of a calculus of capabilities
A Charguéraud, F Pottier
Proceedings of the 13th ACM SIGPLAN international conference on Functional …, 2008
732008
Program verification through characteristic formulae
A Charguéraud
Proceedings of the 15th ACM SIGPLAN International Conference on Functional …, 2010
682010
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
632018
Separation logic for sequential programs (functional pearl)
A Charguéraud
Proceedings of the ACM on Programming Languages 4 (ICFP), 1-34, 2020
502020
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
432015
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
342019
Oracle scheduling: Controlling granularity in implicitly parallel languages
UA Acar, A Charguéraud, M Rainey
ACM Sigplan Notices 46 (10), 499-518, 2011
332011
Formal proof and analysis of an incremental cycle detection algorithm
A Guéneau, JH Jourdan, A Charguéraud, F Pottier
Interactive Theorem Proving, 2019
312019
Temporary read-only permissions for separation logic
A Charguéraud, F Pottier
Programming Languages and Systems: 26th European Symposium on Programming …, 2017
312017
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
292015
Characteristic formulae for mechanized program verification
A Charguéraud
PhD thesis, Université Paris 7, 2010
282010
JSExplain: A double debugger for JavaScript
A Charguéraud, A Schmitt, T Wood
Companion Proceedings of the The Web Conference 2018, 691-699, 2018
272018
The system can't perform the operation now. Try again later.
Articles 1–20