{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:59Z","timestamp":1780994699162,"version":"3.54.1"},"reference-count":74,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ERC","award":["101096090"],"award-info":[{"award-number":["101096090"]}]},{"name":"NSF","award":["2318724"],"award-info":[{"award-number":["2318724"]}]},{"DOI":"10.13039\/100008398","name":"VILLUM Foundation","doi-asserted-by":"crossref","award":["25804"],"award-info":[{"award-number":["25804"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n            Probabilistic couplings are the foundation for many probabilistic relational program logics and arise when relating random sampling statements across two programs. In relational program logics, this manifests as dedicated coupling rules that,\n            <jats:italic toggle=\"yes\">e.g<\/jats:italic>\n            ., say we may reason as if two sampling statements return the same value. However, this approach fundamentally requires aligning or \u201csynchronizing\u201d the sampling statements of the two programs which is not always possible.\n          <\/jats:p>\n          <jats:p>\n            In this paper, we develop Clutch, a higher-order probabilistic relational separation logic that addresses this issue by supporting\n            <jats:italic toggle=\"yes\">asynchronous<\/jats:italic>\n            probabilistic couplings. We use Clutch to develop a logical step-indexed logical relation to reason about contextual refinement and equivalence of higher-order programs written in a rich language with a probabilistic choice operator, higher-order local state, and impredicative polymorphism. Finally, we demonstrate our approach on a number of case studies.\n          <\/jats:p>\n          <jats:p>All the results that appear in the paper have been formalized in the Coq proof assistant using the Coquelicot library and the Iris separation logic framework.<\/jats:p>","DOI":"10.1145\/3632868","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"753-784","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["Asynchronous Probabilistic Couplings in Higher-Order Separation Logic"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6045-5232","authenticated-orcid":false,"given":"Simon Oddershede","family":"Gregersen","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6746-2734","authenticated-orcid":false,"given":"Alejandro","family":"Aguirre","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0198-7751","authenticated-orcid":false,"given":"Philipp G.","family":"Haselwarter","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5692-3347","authenticated-orcid":false,"given":"Joseph","family":"Tassarotti","sequence":"additional","affiliation":[{"name":"New York University, New York City, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5115"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00048"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_8"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473598"},{"key":"e_1_3_1_7_1","first-page":"243","article-title":"Random walks on finite groups and rapidly mixing Markov chains","volume":"17","author":"Aldous David J.","year":"1983","unstructured":"David J. Aldous. 1983. Random walks on finite groups and rapidly mixing Markov chains. S\u00e9minaire de probabilit\u00e9s de Strasbourg 17 (1983), 243\u2013297. http:\/\/www.numdam.org\/item\/SPS_1983__17__243_0\/","journal-title":"S\u00e9minaire de probabilit\u00e9s de Strasbourg"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363211"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932501"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470712"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498719"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484548"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Elaine B. Barker and John M. Kelsey. 2015. Recommendation for Random Number Generation Using Deterministic Random Bit Generators. National Institute of Standards and Technology. https:\/\/doi.org\/10.6028\/nist.sp.800-90ar1 10.6028\/nist.sp.800-90ar1","DOI":"10.6028\/nist.sp.800-90ar1"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Fran\u00e7ois Dupressoir Benjamin Gr\u00e9goire C\u00e9sar Kunz Benedikt Schmidt and Pierre-Yves Strub. 2013. EasyCrypt: A Tutorial. In Foundations of Security Analysis and Design VII - FOSAD 2012\/2013 Tutorial Lectures. 146\u2013166. https:\/\/doi.org\/10.1007\/978-3-319-10082-1_6 10.1007\/978-3-319-10082-1_6","DOI":"10.1007\/978-3-319-10082-1_6"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_27"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158145"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978391"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_10"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371123"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103670"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/168588.168596"},{"key":"e_1_3_1_25_1","unstructured":"Mihir Bellare and Phillip Rogaway. 2004. Code-Based Game-Playing Proofs and the Security of Triple Encryption. Cryptology ePrint Archive Paper 2004\/331. https:\/\/eprint.iacr.org\/2004\/331 https:\/\/eprint.iacr.org\/2004\/331."},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11761679_25"},{"key":"e_1_3_1_27_1","unstructured":"Ale\u0161 Bizjak. 2016. On Semantics and Applications of Guarded Recursion. Ph. D. Dissertation. Aarhus University."},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_18"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-014-0181-1"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1162\/153244302760200704"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2021.09.027"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498680"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:16)2011"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681200024X"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1561\/0400000042"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1985.1057074"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00003"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:9)2021"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571223"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527318"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90070-9"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","unstructured":"Simon Oddershede Gregersen Alejandro Aguirre Philipp G. Haselwarter Joseph Tassarotti and Lars Birkedal. 2023a. Asynchronous Probabilistic Couplings in Higher-Order Separation Logic - Coq Artifact. https:\/\/doi.org\/10.5281\/zenodo 10.5281\/zenodo","DOI":"10.5281\/zenodo"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","unstructured":"Simon Oddershede Gregersen Alejandro Aguirre Philipp G. Haselwarter Joseph Tassarotti and Lars Birkedal. 2023b. Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. CoRR abs\/2301.10061 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2301.10061 10.48550\/ARXIV.2301.10061 arXiv:2301.10061","DOI":"10.48550\/ARXIV.2301.10061"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434291"},{"key":"e_1_3_1_47_1","unstructured":"Philipp G. Haselwarter Exequiel Rivas Antoine Van Muylder Th\u00e9o Winterhalter Carmine Abate Nikolaj Sidorenco Catalin Hritcu Kenji Maillard and Bas Spitters. 2021. SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. Cryptology ePrint Archive Paper 2021\/397. https:\/\/eprint.iacr.org\/2021\/397 https:\/\/eprint.iacr.org\/2021\/397."},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","unstructured":"Patricia Johann Alex Simpson and Janis Voigtl\u00e4nder. 2010. A Generic Operational Metatheory for Algebraic Effects. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science LICS 2010 11-14 July 2010 Edinburgh United Kingdom. 209\u2013218. https:\/\/doi.org\/10.1109\/LICS.2010.29 10.1109\/LICS.2010.29","DOI":"10.1109\/LICS.2010.29"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_1_55_1","volume-title":"Lectures on the Coupling Method","author":"Lindvall T.","year":"2002","unstructured":"T. Lindvall. 2002. Lectures on the Coupling Method. Dover Publications, Incorporated."},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-63287-8"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46666-7_4"},{"key":"e_1_3_1_58_1","first-page":"227","volume-title":"Higher Order Operational Techniques in Semantics","author":"Pitts Andrew M.","year":"1998","unstructured":"Andrew M. Pitts and Ian D. B. Stark. 1998. Operational Reasoning for Functions with Local State. In Higher Order Operational Techniques in Semantics, A. D. Gordon and A. M. Pitts (Eds.). Cambridge University Press, 227\u2013273."},{"key":"e_1_3_1_59_1","unstructured":"Mike Rosulek. 2020. The Joy of Cryptography. http:\/\/web.engr.oregonstate.edu\/~rosulekm\/crypto\/"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837651"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01940876"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/9783-642-54833-8_9"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2022. The Coq Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.7313584 10.5281\/zenodo.7313584","DOI":"10.5281\/zenodo.7313584"},{"key":"e_1_3_1_65_1","unstructured":"The Iris Development Team. 2022. The Iris 4.0 Reference. https:\/\/plv.mpi-sws.org\/iris\/appendix-4.0.pdf"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1236-2"},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341709"},{"key":"e_1_3_1_68_1","unstructured":"Amin Timany Simon Oddershede Gregersen L\u00e9o Stefanesco L\u00e9on Gondelman Abel Nieto and Lars Birkedal. 2021. Trillium: Unifying Refinement and Higher-Order Distributed Separation Logic. CoRR abs\/2109.07863 (2021). arXiv:2109.07863 https:\/\/arxiv.org\/abs\/2109.07863"},{"key":"e_1_3_1_69_1","unstructured":"Amin Timany Robbert Krebbers Derek Dreyer and Lars Birkedal. 2022. A Logical Approach to Type Soundness. (2022). https:\/\/iris-project.org\/pdfs\/2022-submitted-logical-type-soundness.pdf Unpublished manuscript."},{"key":"e_1_3_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_3_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429111"},{"key":"e_1_3_1_73_1","volume-title":"Optimal Transport: Old and New","author":"Villani C.","year":"2008","unstructured":"C. Villani. 2008. Optimal Transport: Old and New. Springer Berlin Heidelberg."},{"key":"e_1_3_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236782"},{"key":"e_1_3_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498677"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632868","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632868","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:02:45Z","timestamp":1751659365000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632868"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":74,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632868"],"URL":"https:\/\/doi.org\/10.1145\/3632868","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}