Arthur Charguéraud

Cited by

	All	Since 2020
Citations	2145	1031
h-index	23	17
i10-index	31	24

240

120

180

20082009201020112012201320142015201620172018201920202021202220232024202527 36 47 58 55 63 91 76 120 128 149 225 157 217 207 217 197 35

Public access

View all

19 articles

0 articles

available

not available

Based on funding mandates

Co-authors

Mike RaineyCarnegie Mellon UniversityVerified email at mike-rainey.site
Umut A. AcarCarnegie Mellon University, Department of Computer ScienceVerified email at cs.cmu.edu
François PottierInria ParisVerified email at inria.fr
Martin BodinInriaVerified email at ens-lyon.org
Jacques-Henri JourdanCNRS, Laboratoire Méthodes FormellesVerified email at cnrs.fr
Alan SchmittInria, IRISAVerified email at inria.fr
Mário PereiraAssistant Professor, NOVA School of Science and TechnologyVerified email at fct.unl.pt
Jean-Christophe FilliâtreCNRSVerified email at lri.fr
Benjamin C. PierceProfessor of Computer and Information Science, University of PennsylvaniaVerified email at cis.upenn.edu
Stephanie WeirichProfessor of Computer Science, University of PennsylvaniaVerified email at cis.upenn.edu
Philippa GardnerProfessor of Theoretical Computer Science, Imperial College LondonVerified email at imperial.ac.uk
Sergio MaffeisSenior Lecturer (Associate Professor) in Computer Security, Imperial College LondonVerified email at doc.ic.ac.uk
Robbert KrebbersAssociate Professor, Radboud University NijmegenVerified email at cs.ru.nl
Amin TimanyAarhus UniversityVerified email at cs.au.dk
Joseph TassarottiAssistant Professor, New York UniversityVerified email at nyu.edu
Derek DreyerMax Planck Institute for Software Systems (MPI-SWS), Saarland Informatics CampusVerified email at mpi-sws.org
Ralf JungAssistant Professor, ETH ZürichVerified email at inf.ethz.ch
Filip SieczkowskiHeriot-Watt UniversityVerified email at hw.ac.uk
Alexandre MoineNew York UniversityVerified email at nyu.edu
Samuel GruetterMITVerified email at mit.edu

Arthur Charguéraud

Inria

Verified email at inria.fr

Programming Languages and Formal Proofs


Title Sort by citations Sort by year Sort by 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	309	2008
The locally nameless representation A Charguéraud Journal of automated reasoning 49, 363-408, 2012	235	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	178	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	176	2014
Characteristic formulae for the verification of imperative programs A Charguéraud Proceedings of the 16th ACM SIGPLAN international conference on Functional …, 2011	148	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	114	2018
Pretty-big-step semantics A Charguéraud European Symposium on Programming, 41-60, 2013	103	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	89	2019
Functional translation of a calculus of capabilities A Charguéraud, F Pottier Proceedings of the 13th ACM SIGPLAN international conference on Functional …, 2008	73	2008
Program verification through characteristic formulae A Charguéraud Proceedings of the 15th ACM SIGPLAN International Conference on Functional …, 2010	68	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	63	2018
Separation logic for sequential programs (functional pearl) A Charguéraud Proceedings of the ACM on Programming Languages 4 (ICFP), 1-34, 2020	51	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	43	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	38	2019
Oracle scheduling: Controlling granularity in implicitly parallel languages UA Acar, A Charguéraud, M Rainey ACM Sigplan Notices 46 (10), 499-518, 2011	33	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	32	2019
Temporary read-only permissions for separation logic A Charguéraud, F Pottier Programming Languages and Systems: 26th European Symposium on Programming …, 2017	32	2017
JSExplain: A double debugger for JavaScript A Charguéraud, A Schmitt, T Wood Companion Proceedings of the The Web Conference 2018, 691-699, 2018	29	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	29	2015
Characteristic formulae for mechanized program verification A Charguéraud PhD thesis, Université Paris 7, 2010	28	2010

The system can't perform the operation now. Try again later.

Articles 1–20

Citations per year

Duplicate citations

Merged citations

Add co-authorsCo-authors

Follow

Cited by

Co-authors