{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T02:25:44Z","timestamp":1784255144661,"version":"3.55.0"},"reference-count":54,"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\/4.0\/"}],"funder":[{"name":"ANR","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":[[2025,1,7]]},"abstract":"<jats:p>\n                    We introduce\n                    <jats:monospace>eRHL<\/jats:monospace>\n                    , a program logic for reasoning about relational expectation properties of pairs of probabilistic programs. eRHL is quantitative, i.e., its pre- and post-conditions take values in the extended non-negative reals. Thanks to its quantitative assertions,\n                    <jats:monospace>eRHL<\/jats:monospace>\n                    overcomes randomness alignment restrictions from prior logics, including\n                    <jats:monospace>pRHL<\/jats:monospace>\n                    , a popular relational program logic used to reason about security of cryptographic constructions, and\n                    <jats:monospace>apRHL<\/jats:monospace>\n                    , a variant of\n                    <jats:monospace>pRHL<\/jats:monospace>\n                    for differential privacy. As a result,\n                    <jats:monospace>eRHL<\/jats:monospace>\n                    is the first relational probabilistic program logic to be supported by non-trivial soundness and completeness results for all\n                    <jats:italic toggle=\"yes\">almost surely terminating<\/jats:italic>\n                    programs. We show that\n                    <jats:monospace>eRHL<\/jats:monospace>\n                    is sound and complete with respect to program equivalence, statistical distance, and differential privacy. We also show that every\n                    <jats:monospace>pRHL<\/jats:monospace>\n                    judgment is valid iff it is provable in\n                    <jats:monospace>eRHL<\/jats:monospace>\n                    . We showcase the practical benefits of\n                    <jats:monospace>eRHL<\/jats:monospace>\n                    with examples that are beyond reach of\n                    <jats:monospace>pRHL<\/jats:monospace>\n                    and\n                    <jats:monospace>apRHL<\/jats:monospace>\n                    .\n                  <\/jats:p>","DOI":"10.1145\/3704876","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1167-1195","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["A Quantitative Probabilistic Relational Hoare Logic"],"prefix":"10.1145","volume":"9","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":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3853-1777","authenticated-orcid":false,"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"MPI-SP + IMDEA Software Institute, Spain, Bochum, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-2981-2962","authenticated-orcid":false,"given":"Davide","family":"Davoli","sequence":"additional","affiliation":[{"name":"Centre Inria d'Universit\u00e9 C\u00f4te d'Azur, Sophia Antipolis, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"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.1007\/978-3-319-89884-1_8"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434333"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158146"},{"issue":"8","key":"e_1_3_2_5_1","article-title":"Hopping Proofs of ExpectationBased Properties: Applications to Skiplists and Security Proofs","author":"Avanzini Martin","year":"2024","unstructured":"Martin Avanzini, Gilles Barthe, Benjamin Gr\u00e9goire, Georg Moser, and Gabriele Vanoni. 2024. Hopping Proofs of ExpectationBased Properties: Applications to Skiplists and Security Proofs. Proc. PACMPL (2024). Issue 8(OOPSLA).","journal-title":"Proc. PACMPL"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2402.18708"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484567"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394796"},{"key":"e_1_3_2_9_1","article-title":"Relational reasoning via probabilistic coupling","author":"Barthe Gilles","year":"2015","unstructured":"Gilles Barthe, Thomas Espitau, Benjamin Gr\u00e9goire, Justin Hsu, L\u00e9o Stefanesco, and Pierre-Yves Strub. 2015. Relational reasoning via probabilistic coupling. CoRR abs\/1509.03476 (2015). arXiv: 1509.03476 http:\/\/www.arxiv.org\/abs\/1509.03476","journal-title":"CoRR"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158145"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-15(4:18)2019"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978391"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Benjamin Gr\u00e9goire and Santiago Zanella B\u00e9guelin. 2009. Formal Certification of Code-based Cryptographic Proofs. 90-101. https:\/\/doi.org\/10.1145\/1480881.1480894 10.1145\/1480881.1480894","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Benjamin Gr\u00e9goire Justin Hsu and Pierre-Yves Strub. 2017. Coupling proofs are probabilistic product programs Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM 161-174. https:\/\/doi.org\/10.1145\/1480881.1480894 10.1145\/1480881.1480894","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371089"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103670"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_8"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/S00145-019-09341-Z"},{"key":"e_1_3_2_21_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:\/\/www.eprint.iacr.org\/2004\/331"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243863"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1162\/153244302760200704"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623170"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2404.03430"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243818"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11761679_29"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11681878_14"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1561\/0400000042"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632868"},{"key":"e_1_3_2_31_1","unstructured":"Moritz Hardt Benjamin Recht and Yoram Singer. 2016. Train faster generalize better: stability of stochastic gradient descent. In Proceedings of the 33rd International Conference on International Conference on Machine Learning - Volume 48 (New York NY USA) (ICML'16). http:\/\/www.JMLR.org 1225-1234."},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371105"},{"key":"e_1_3_2_33_1","unstructured":"Justin Hsu . 2017. Probabilistic Couplings for Probabilistic Reasoning. Ph. D. Dissertation. University of Pennsylvania. http:\/\/arxiv.org\/abs\/1710.09951"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","unstructured":"Benjamin Lucien Kaminski and Joost-Pieter Katoen. 2017. A Weakest Pre-expectation Semantics for Mixed-sign Expectations. 1-12. https:\/\/doi.org\/10.1109\/LICS.2017.8005153 10.1109\/LICS.2017.8005153","DOI":"10.1109\/LICS.2017.8005153"},{"issue":"7","key":"e_1_3_2_35_1","first-page":"52","article-title":"On a space of totally additive functions","volume":"13","author":"Kantorovich Leonid Vasilevich","year":"1958","unstructured":"Leonid Vasilevich Kantorovich and SG Rubinshtein. 1958. On a space of totally additive functions. Vestnik of the St. Petersburg University: Mathematics 13, 7 (1958), 52-59.","journal-title":"Vestnik of the St. Petersburg University: Mathematics"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2008.27"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_51"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_3_2_39_1","volume-title":"Markov chains and mixing times","author":"Levin David A.","year":"2009","unstructured":"David A. Levin, Yuval Peres, and Elizabeth L. Wilmer. 2009. Markov chains and mixing times. American Mathematical Society."},{"key":"e_1_3_2_40_1","volume-title":"Lectures on the coupling method","author":"Lindvall Torgny","year":"2002","unstructured":"Torgny Lindvall . 2002. Lectures on the coupling method. Courier Corporation."},{"key":"e_1_3_2_41_1","volume-title":"Abstraction, refinement and proof for probabilistic systems","author":"McIver Annabelle","year":"2005","unstructured":"Annabelle McIver and Carroll Morgan. 2005. Abstraction, refinement and proof for probabilistic systems. Springer Science & Business Media."},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-010-0413-8_11"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","unstructured":"Federico Olmedo Benjamin Lucien Kaminski Joost-Pieter Katoen and Christoph Matheja. 2016. Reasoning about Recursive Probabilistic Programs. 672-681. https:\/\/doi.org\/10.1145\/2933575.2935317 10.1145\/2933575.2935317","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46666-7_4"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2016.09.043"},{"key":"e_1_3_2_47_1","unstructured":"Adam D. Smith . 2009. Differential privacy and the secrecy of the sample. https:\/\/www.adamdsmith.wordpress.com\/2009\/09\/02\/sample-secrecy\/"},{"key":"e_1_3_2_48_1","unstructured":"Thomas Steinke . 2022. Composition of Differential Privacy & Privacy Amplification by Subsampling. arXiv:2210.00597 [cs.CR] https:\/\/arxiv.org\/abs\/2210.00597"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177700153"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547643"},{"key":"e_1_3_2_53_1","doi-asserted-by":"crossref","unstructured":"Cedric Villani . 2008. Optimal transport: old and new.","DOI":"10.1007\/978-3-540-71050-9"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371093"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1965.10480775"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704876","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704876","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:18:25Z","timestamp":1770200305000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704876"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":54,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704876"],"URL":"https:\/\/doi.org\/10.1145\/3704876","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"}}]}}