{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:09Z","timestamp":1780994709030,"version":"3.54.1"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["2338317"],"award-info":[{"award-number":["2338317"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002808","name":"Carlsbergfondet","doi-asserted-by":"publisher","award":["CF23-0791"],"award-info":[{"award-number":["CF23-0791"]}],"id":[{"id":"10.13039\/501100002808","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["25804"],"award-info":[{"award-number":["25804"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101096090"],"award-info":[{"award-number":["101096090"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>Properties such as provable security and correctness for randomized programs are naturally expressed relationally as approximate equivalences. As a result, a number of relational program logics have been developed to reason about such approximate equivalences of probabilistic programs. However, existing approximate relational logics are mostly restricted to first-order programs without general state.<\/jats:p>\n                  <jats:p>\n                    In this paper we develop Approxis, a\n                    <jats:italic toggle=\"yes\">higher-order approximate relational separation logic<\/jats:italic>\n                    for reasoning about approximate equivalence of programs written in an expressive ML-like language with discrete probabilistic sampling, higher-order functions, and higher-order state. The Approxis logic recasts the concept of\n                    <jats:italic toggle=\"yes\">error credits<\/jats:italic>\n                    in the relational setting to reason about relational approximation, which allows for expressive notions of modularity and composition, a range of new approximate relational rules, and an internalization of a standard limiting argument for showing exact probabilistic equivalences by approximation. We also use Approxis to develop a logical relation model that quantifies over error credits, which can be used to prove\n                    <jats:italic toggle=\"yes\">exact contextual equivalence<\/jats:italic>\n                    . We demonstrate the flexibility of our approach on a range of examples, including the PRP\/PRF switching lemma, IND$-CPA security of an encryption scheme, and a collection of rejection samplers. All of the results have been mechanized in the Coq proof assistant and the Iris separation logic framework.\n                  <\/jats:p>","DOI":"10.1145\/3704877","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1196-1226","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Approximate Relational Reasoning for Higher-Order Probabilistic Programs"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0198-7751","authenticated-orcid":false,"given":"Philipp G.","family":"Haselwarter","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4124-5720","authenticated-orcid":false,"given":"Kwing Hei","family":"Li","sequence":"additional","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-0001-6045-5232","authenticated-orcid":false,"given":"Simon Oddershede","family":"Gregersen","sequence":"additional","affiliation":[{"name":"New York University, New York, USA"}],"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, 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":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00048"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473598"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571195"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674635"},{"key":"e_1_3_2_6_1","unstructured":"Jos\u00e9 Bacelar Almeida Denis Firsov Tiago Oliveira and Dominique Unruh. 2023. Leakage-Free Probabilistic Jasmin Programs. Cryptology ePrint Archive Paper 2023\/1514. https:\/\/www.eprint.iacr.org\/2023\/1514 https:\/\/www.eprint.iacr.org\/2023\/1514."},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:17)2011"},{"key":"e_1_3_2_8_1","unstructured":"Martin Avanzini Gilles Barthe Davide Davoli and Benjamin Gr\u00e9goire. 2024. A quantitative probabilistic relational Hoare logic. arXiv:2407.17127 [cs.LO] https:\/\/www.arxiv.org\/abs\/2407.17127"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470712"},{"key":"e_1_3_2_10_1","unstructured":"Jialu Bao Emanuele D'Osualdo and Azadeh Farzan. 2024. Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning. arXiv:2402.18708 [cs.LO] https:\/\/www.arxiv.org\/abs\/2402.18708"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498719"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10082-1_6"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_27"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158145"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978391"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2016.107"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480894"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_10"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371123"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103670"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571260"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00288683"},{"key":"e_1_3_2_25_1","first-page":"331","article-title":"Code-Based Game-Playing Proofs and the Security of Triple Encryption","volume":"2004","author":"Bellare Mihir","year":"2004","unstructured":"Mihir Bellare and Phillip Rogaway. 2004. Code-Based Game-Playing Proofs and the Security of Triple Encryption. IACR Cryptol. ePrint Arch. (2004), 331. http:\/\/eprint.iacr.org\/2004\/331","journal-title":"IACR Cryptol. ePrint Arch."},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_18"},{"key":"e_1_3_2_28_1","volume-title":"Workshop on the link between formal and computational models","author":"Blanchet Bruno","year":"2005","unstructured":"Bruno Blanchet . 2005. A Computationally Sound Automatic Prover for Cryptographic Protocols. In Workshop on the link between formal and computational models. Paris, France."},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/S11786-014-0181-1"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03332-3_9"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9431-7"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_13"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.64"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_14"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571259"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:9)2021"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90070-9"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2301.10061"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632868"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0055742"},{"key":"e_1_3_2_41_1","unstructured":"Philipp G. Haselwarter Kwing Hei Li Alejandro Aguirre Simon Oddershede Gregersen Joseph Tassarotti and Lars Birkedal. 2024a. Approximate Relational Reasoning for Higher-Order Probabilistic Programs. arXiv:2407.14107 [cs.LO] https:\/\/www.arxiv.org\/abs\/2407.14107"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","unstructured":"Philipp G. Haselwarter Kwing Hei Li Alejandro Aguirre Simon Oddershede Gregersen Joseph Tassarotti and Lars Birkedal. 2024b. Approximate Relational Reasoning for Higher-Order Probabilistic Programs - Formalization Artifact. https:\/\/doi.org\/10.5281\/zenodo.13939302 10.5281\/zenodo.13939302","DOI":"10.5281\/zenodo.13939302"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689753"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3594735"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/640128.604148"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_3_2_49_1","volume-title":"Introduction to Modern Cryptography","author":"Katz Jonathan","year":"2021","unstructured":"Jonathan Katz and Yehuda Lindell. 2021. Introduction to Modern Cryptography (third ed.). CRC Press."},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591226"},{"key":"e_1_3_2_51_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_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371072"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192394"},{"key":"e_1_3_2_56_1","first-page":"269","article-title":"Random Sampling from B+ Trees","author":"Olken Frank","year":"1989","unstructured":"Frank Olken and Doron Rotem. 1989. Random Sampling from B+ Trees. In Proceedings of the Fifteenth International Conference on Very Large Data Bases. 269-277. http:\/\/www.vldb.org\/conf\/1989\/P269.PDF","journal-title":"In Proceedings of the Fifteenth International Conference on Very Large Data Bases."},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632892"},{"key":"e_1_3_2_58_1","unstructured":"Mike Rosulek . 2021. The Joy of Cryptography."},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2016.09.043"},{"key":"e_1_3_2_60_1","unstructured":"Victor Shoup . 2004. Sequences ofGames: A Tool for Taming Complexity in Security Proofs. https:\/\/www.eprint.iacr.org\/2004\/332"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2024. The Coq Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.11551307 10.5281\/zenodo.11551307","DOI":"10.5281\/zenodo.11551307"},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1236-2"},{"key":"e_1_3_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3676954"},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_3_2_65_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_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236782"},{"key":"e_1_3_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408992"},{"key":"e_1_3_2_68_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\/3704877","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704877","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:18:21Z","timestamp":1770200301000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704877"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":67,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704877"],"URL":"https:\/\/doi.org\/10.1145\/3704877","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}