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
2382008
The locally nameless representation
A Charguéraud
Journal of automated reasoning 49 (3), 363-408, 2012
1402012
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
1152013
A trusted mechanised JavaScript specification
M Bodin, A Charguéraud, D Filaretti, P Gardner, S Maffeis, ...
ACM SIGPLAN Notices 49 (1), 87-100, 2014
992014
Characteristic formulae for the verification of imperative programs
A Charguéraud
Proceedings of the 16th ACM SIGPLAN international conference on Functional …, 2011
952011
Functional translation of a calculus of capabilities
A Charguéraud, F Pottier
Proceedings of the 13th ACM SIGPLAN international conference on Functional …, 2008
702008
Pretty-big-step semantics
A Charguéraud
European Symposium on Programming, 41-60, 2013
622013
Program verification through characteristic formulae
A Charguéraud
Proceedings of the 15th ACM SIGPLAN international conference on Functional …, 2010
442010
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
362015
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
332019
Oracle scheduling: Controlling granularity in implicitly parallel languages
UA Acar, A Charguéraud, M Rainey
ACM Sigplan Notices 46 (10), 499-518, 2011
292011
Characteristic formulae for mechanized program verification
A Charguéraud
PhD thesis, Université Paris-Diderot, 2010
262010
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
202018
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
182018
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
162015
Temporary read-only permissions for separation logic
A Charguéraud, F Pottier
European Symposium on Programming, 260-286, 2017
142017
Oracle-guided scheduling for controlling granularity in implicitly parallel languages
U Acar, A Charguéraud, M Rainey
142016
Theory and practice of chunked sequences
UA Acar, A Charguéraud, M Rainey
European Symposium on Algorithms, 25-36, 2014
132014
Higher-order representation predicates in separation logic
A Charguéraud
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and …, 2016
122016
Formal proof and analysis of an incremental cycle detection algorithm
A Guéneau, JH Jourdan, A Charguéraud, F Pottier
112019
The system can't perform the operation now. Try again later.
Articles 1–20