{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:24:49Z","timestamp":1770279889869,"version":"3.49.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T00:00:00Z","timestamp":1714348800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Agence Nationale pour la Recherche","award":["ANR-19-CE48-0014 ANR-22-PECY-0006"],"award-info":[{"award-number":["ANR-19-CE48-0014 ANR-22-PECY-0006"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,4,29]]},"abstract":"<jats:p>We propose, implement, and evaluate a hopping proof approach for  \n proving expectation-based properties of probabilistic programs. Our  \n approach combines EHL, a syntax-directed proof system for reducing  \n proof goals of a program to proof goals of simpler programs, with a  \n \"hopping\" proof rule for reducing proof goals of an  \n original program to proof goal of a different program which is  \n suitably related (by means of pRHL, a relational program logic for  \n probabilistic program) to the original program. We prove that EHL  \n is sound for a core language with procedure calls and adversarial  \n computations, and complete for the adversary-free fragment of the  \n language. We also provide an implementation of EHL into  \n EasyCrypt, a proof assistant tailored for reasoning about  \n relational properties of probabilistic programs. We provide a tight  \n integration of EHL with other program logics supported by  \n EasyCrypt, and in particular probabilistic Relational Hoare Logic  \n (pRHL). Using this tight integration, we give mechanized proofs of  \n expected complexity of in-place implementations of randomized  \n quickselect and skip lists. We also sketch applications of our  \n approach to cryptographic proofs and discuss the broader impact of  \n EHL in the EasyCrypt proof assistant.<\/jats:p>","DOI":"10.1145\/3649839","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"784-809","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6445-8833","authenticated-orcid":false,"given":"Martin","family":"Avanzini","sequence":"first","affiliation":[{"name":"Centre Inria d?Universit\u00e9 C\u00f4te d?Azur, Sophia-Antipolis, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3853-1777","authenticated-orcid":false,"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"MPI-SP, Bochum, Germany \/ IMDEA Software Institute, Madrid, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6650-9924","authenticated-orcid":false,"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[{"name":"Centre Inria d?Universit\u00e9 C\u00f4te d?Azur, Sophia-Antipolis, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9240-6128","authenticated-orcid":false,"given":"Georg","family":"Moser","sequence":"additional","affiliation":[{"name":"University of Innsbruck, Innsbruck, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8762-8674","authenticated-orcid":false,"given":"Gabriele","family":"Vanoni","sequence":"additional","affiliation":[{"name":"Centre Inria d?Universit\u00e9 C\u00f4te d?Azur, Sophia-Antipolis, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","unstructured":"S. Agrawal K. Chatterjee and P. Novotn\u00fd. 2018. Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs. PACMPL 2 POPL (2018) 34:1\u201334:32. https:\/\/doi.org\/10.1145\/3385412.3386002 10.1145\/3385412.3386002","DOI":"10.1145\/3385412.3386002"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","unstructured":"Martin Avanzini Gilles Barthe Benjamin Gr\u00e9goire Georg Moser and Gabriele Vanoni. 2024. ehoare.tar.gz. https:\/\/doi.org\/10.5281\/zenodo.10517828 10.5281\/zenodo.10517828","DOI":"10.5281\/zenodo.10517828"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473592"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785725"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2019.102338"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428240"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591263"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-38554-4_12"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484548"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10082-1_6"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_3"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_27"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31113-0_1"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009896"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571260"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_11"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054112400588"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_6"},{"key":"e_1_2_1_21_1","volume-title":"Introduction to Algorithms","author":"Cormen Thomas H.","unstructured":"Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms, 3rd Edition. MIT Press.","edition":"3"},{"key":"e_1_2_1_22_1","unstructured":"L\u00e1o Ducas Eike Kiltz Tancr\u00e8de Lepoint Vadim Lyubashevsky Peter Schwabe Gregor Seiler and Damien Stehl\u00e9. 2017. CRYSTALS\u2013Dilithium: Algorithm Specification and Supporting Documentation. Round-1 submission to the NIST Post-Quantum Cryptography Standardization Project. https:\/\/cryptojedi.org\/papers\/#dilithium"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09545-0"},{"key":"e_1_2_1_24_1","unstructured":"Maximilian Paul Louis Haslbeck. 2021. Verified Quantitative Analysis of Imperative Algorithms. Ph. D. Dissertation. Technische Universit\u00e4t M\u00fcnchen."},{"key":"e_1_2_1_25_1","first-page":"2020","volume-title":"Skip Lists. Arch. Formal Proofs","author":"Max","year":"2020","unstructured":"Max W. Haslbeck and Manuel Eberl. 2020. Skip Lists. Arch. Formal Proofs, 2020 (2020), https:\/\/www.isa-afp.org\/entries\/Skip_Lists.html"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/366622.366647"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.01.021"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","unstructured":"B. L. Kaminski J.-P. Katoen C. Matheja and F. Olmedo. 2018. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. JACM 65 5 (2018) 30:1\u201330:68. https:\/\/doi.org\/10.1145\/3208102 10.1145\/3208102","DOI":"10.1145\/3208102"},{"key":"e_1_2_1_31_1","volume-title":"Hoare logic and VDM : machine-checked soundness and completeness proofs. Ph. D. Dissertation","author":"Kleymann Thomas","year":"1842","unstructured":"Thomas Kleymann. 1998. Hoare logic and VDM : machine-checked soundness and completeness proofs. Ph. D. Dissertation. University of Edinburgh, UK. http:\/\/hdl.handle.net\/1842\/387"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050057"},{"key":"e_1_2_1_33_1","volume-title":"Sorting And Searching","author":"Knuth Donald","unstructured":"Donald Knuth. 1973. The Art Of Computer Programming, vol. 3: Sorting And Searching. Addison-Wesley."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_12"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_4"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706326"},{"key":"e_1_2_1_38_1","volume-title":"refinement and proof for probabilistic systems","author":"McIver Annabelle","unstructured":"Annabelle McIver and Carroll Morgan. 2005. Abstraction, refinement and proof for probabilistic systems. Springer Science & Business Media."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192394"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45793-3_8"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-010-0413-8_11"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59152-6_2"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3156018"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_2_1_46_1","unstructured":"William Pugh. 1990. Concurrent Maintenance of Skip Lists. USA. http:\/\/hdl.handle.net\/1903\/542"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/78973.78977"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_28"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_33"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02444-3_16"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408992"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314581"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649839","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649839","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:06Z","timestamp":1750287246000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649839"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":53,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649839"],"URL":"https:\/\/doi.org\/10.1145\/3649839","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,29]]},"assertion":[{"value":"2024-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}