| Engineering formal metatheory B Aydemir, A Charguéraud, BC Pierce, R Pollack, S Weirich Acm sigplan notices 43 (1), 3-15, 2008 | 331 | 2008 |
| The locally nameless representation A Charguéraud Journal of automated reasoning 49 (3), 363-408, 2012 | 293 | 2012 |
| 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 | 193 | 2014 |
| 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 | 187 | 2013 |
| Characteristic formulae for the verification of imperative programs A Charguéraud Proceedings of the 16th ACM SIGPLAN international conference on Functional …, 2011 | 171 | 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 | 150 | 2018 |
| Pretty-big-step semantics A Charguéraud European Symposium on Programming, 41-60, 2013 | 115 | 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 | 109 | 2019 |
| Program verification through characteristic formulae A Charguéraud Proceedings of the 15th ACM SIGPLAN International Conference on Functional …, 2010 | 79 | 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 | 78 | 2018 |
| Functional translation of a calculus of capabilities A Charguéraud, F Pottier Proceedings of the 13th ACM SIGPLAN international conference on Functional …, 2008 | 77 | 2008 |
| Separation logic for sequential programs (functional pearl) A Charguéraud Proceedings of the ACM on Programming Languages 4 (ICFP), 1-34, 2020 | 67 | 2020 |
| GOSPEL—providing OCaml with a formal specification language A Charguéraud, JC Filliâtre, C Lourenço, M Pereira International Symposium on Formal Methods, 484-501, 2019 | 59 | 2019 |
| 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 | 53 | 2015 |
| Formal proof and analysis of an incremental cycle detection algorithm A Guéneau, JH Jourdan, A Charguéraud, F Pottier Interactive Theorem Proving, 2019 | 37 | 2019 |
| Temporary read-only permissions for separation logic A Charguéraud, F Pottier European Symposium on Programming, 260-286, 2017 | 37 | 2017 |
| 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 | 37 | 2015 |
| 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 | 36 | 2018 |
| Oracle scheduling: Controlling granularity in implicitly parallel languages UA Acar, A Charguéraud, M Rainey ACM Sigplan Notices 46 (10), 499-518, 2011 | 36 | 2011 |
| Characteristic formulae for mechanized program verification A Charguéraud PhD thesis, Université Paris 7, 2010 | 33 | 2010 |
Umut A. AcarCarnegie Mellon University, Department of Computer ScienceVerified email at cs.cmu.edu
