{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T14:57:00Z","timestamp":1787065020066,"version":"3.56.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T00:00:00Z","timestamp":1754352000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"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\/100000001","name":"National Science Foundation","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\/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,8,5]]},"abstract":"<jats:p>\n                    We present Coneris, the first\n                    <jats:italic toggle=\"yes\">higher-order concurrent separation logic<\/jats:italic>\n                    for reasoning about error probability bounds of higher-order concurrent probabilistic programs with higher-order state. To support modular reasoning about concurrent (non-probabilistic) program modules, state-of-the-art program logics internalize the classic notion of linearizability within the logic through the concept of\n                    <jats:italic toggle=\"yes\">logical atomicity<\/jats:italic>\n                    . In Coneris, we extend this idea to probabilistic concurrent program modules by capturing a novel notion of\n                    <jats:italic toggle=\"yes\">randomized logical atomicity<\/jats:italic>\n                    within the logic. To do so, Coneris utilizes\n                    <jats:italic toggle=\"yes\">presampling tapes<\/jats:italic>\n                    and a novel\n                    <jats:italic toggle=\"yes\">probabilistic update modality<\/jats:italic>\n                    to describe how state is changed probabilistically at linearization points. We demonstrate this approach by means of smaller synthetic examples and larger case studies. All of the presented results, including the meta-theory, have been mechanized in the Rocq prover and the Iris separation logic framework.\n                  <\/jats:p>","DOI":"10.1145\/3747514","type":"journal-article","created":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:02Z","timestamp":1754412962000},"page":"276-305","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4124-5720","authenticated-orcid":false,"given":"Kwing Hei","family":"Li","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-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-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, 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,8,5]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5115"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3674635"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.29007\/vz48"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978391"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Marco Gaboardi Benjamin Gr\u00e9goire Justin Hsu and Pierre-Yves Strub. 2016. A Program Logic for Union Bounds. In Proceedings of the 43rd International Colloquium on Automata Languages and Programming (ICALP 2016) Ioannis Chatzigiannakis Michael Mitzenmacher Yuval Rabani and Davide Sangiorgi (Eds.). Leibniz International Proceedings in Informatics (LIPIcs) Vol. 55. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik Dagstuhl Germany 107:1\u2013107:15. 10.4230\/LIPIcs.ICALP.2016.107.","DOI":"10.4230\/LIPIcs.ICALP.2016.107"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009896"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31113-0_1"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/2492061"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/168588.168596"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/362686.362692"},{"key":"e_1_3_2_14_2","unstructured":"Sylvie Boldo Catherine Lelay and Guillaume Melquiond. 2013. Coquelicot: A User-Friendly Library of Real Analysis for Coq. (Sept. 2013). https:\/\/inria.hal.science\/hal-00860648 working paper or preprint."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2008.05.018"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2022.25"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993636.1993687"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_16"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632868"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704877"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689753"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926417"},{"key":"e_1_3_2_25_2","first-page":"321","volume-title":"Proceedings Of Ifip Congress \u201983","author":"Jones Cliff","year":"1983","unstructured":"Cliff Jones. 1983. Specification and Design of (Parallel) Programs. Proceedings Of Ifip Congress \u201983, 321\u2013332."},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_29_2","unstructured":"Kwing Hei Li Alejandro Aguirre Simon Oddershede Gregersen Philipp Haselwarter Joseph Tassarotti and Lars Birkedal. 2025. Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version). arXiv:2503.04512 [cs.LO] https:\/\/arxiv.org\/abs\/2503.04512"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Kwing Hei Li Alejandro Aguirre Simon Gregesen Philipp Haselwarter Joseph Tassarotti and Lars Birkedal. 2025. Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs. doi:10.5281\/zenodo.15694473","DOI":"10.5281\/zenodo.15694473"},{"key":"e_1_3_2_31_2","unstructured":"Janine Lohse and Deepak Garg. 2024. An Iris for Expected Cost Analysis. arXiv:2406.00884 [cs.PL]"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.01.016"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-63287-8"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_11"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"The Rocq Development Team. 2024. The Rocq Prover. doi:10.5281\/zenodo.11551307","DOI":"10.5281\/zenodo.11551307"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704855"},{"key":"e_1_3_2_41_2","unstructured":"Noam Zilberstein Alexandra Silva and Joseph Tassarotti. 2024. Probabilistic Concurrent Reasoning in Outcome Logic: Independence Conditioning and Invariants. arXiv:2411.11662 [cs.LO] https:\/\/arxiv.org\/abs\/2411.11662"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3747514","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3747514","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:00:14Z","timestamp":1784196014000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3747514"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,5]]},"references-count":40,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2025,8,5]]}},"alternative-id":["10.1145\/3747514"],"URL":"https:\/\/doi.org\/10.1145\/3747514","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,5]]},"assertion":[{"value":"2025-02-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}