{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:49Z","timestamp":1780994689705,"version":"3.54.1"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","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>We present Coneris, the first *higher-order concurrent separation logic* 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 *logical atomicity*.  \nConeris extends this idea to probabilistic concurrent program modules. Thus Coneris supports modular reasoning about probabilistic concurrent modules by capturing a novel notion of *randomized logical atomicity* within the logic. To do so, Coneris utilizes *presampling tapes* and a novel *probabilistic update modality* to describe how state is changed probabilistically at linearization points. We demonstrate this approach by means of smaller synthetic examples and larger case studies.  \nAll of the presented results, including the meta-theory, have been mechanized in the Rocq proof assistant and the Iris separation logic framework.<\/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":2,"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_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5115"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674635"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.29007\/vz48"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978391"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2016.107"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009896"},{"key":"e_1_2_1_8_1","volume-title":"Mathematics of Program Construction","author":"Barthe Gilles","unstructured":"Gilles Barthe, Benjamin Gr\u00e9goire, and Santiago Zanella B\u00e9guelin. 2012. Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. In Mathematics of Program Construction, Jeremy Gibbons and Pablo Nogueira (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 1\u20136. isbn:978-3-642-31113-0"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2492061"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/168588.168596"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/362686.362692"},{"key":"e_1_2_1_13_1","volume-title":"Coquelicot: A User-Friendly Library of Real Analysis for Coq. Sept., https:\/\/inria.hal.science\/hal-00860648 working paper or preprint","author":"Boldo Sylvie","year":"2013","unstructured":"Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. 2013. Coquelicot: A User-Friendly Library of Real Analysis for Coq. Sept., https:\/\/inria.hal.science\/hal-00860648 working paper or preprint"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.IPL.2008.05.018"},{"key":"e_1_2_1_15_1","volume-title":"TaDA: A Logic for Time and Data Abstraction. In ECOOP 2014 \u2013 Object-Oriented Programming, Richard Jones (Ed.). Springer Berlin Heidelberg","author":"da Rocha Pinto Pedro","year":"2014","unstructured":"Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A Logic for Time and Data Abstraction. In ECOOP 2014 \u2013 Object-Oriented Programming, Richard Jones (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 207\u2013231. isbn:978-3-662-44202-9"},{"key":"e_1_2_1_16_1","volume-title":"Concurrent Abstract Predicates. In ECOOP 2010 \u2013 Object-Oriented Programming, Theo D\u2019Hondt (Ed.). Springer Berlin Heidelberg","author":"Dinsdale-Young Thomas","year":"2010","unstructured":"Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis. 2010. Concurrent Abstract Predicates. In ECOOP 2010 \u2013 Object-Oriented Programming, Theo D\u2019Hondt (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 504\u2013528. isbn:978-3-642-14107-2"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2022.25"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993636.1993687"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_16"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632868"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704877"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689753"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926417"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings Of Ifip Congress \u2019, 83","author":"Jones Cliff","year":"1983","unstructured":"Cliff Jones. 1983. Specification and Design of (Parallel) Programs.. Proceedings Of Ifip Congress \u2019, 83, 321\u2013332."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_28_1","volume-title":"Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal.","author":"Li Kwing Hei","year":"2025","unstructured":"Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal. 2025. Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version). arxiv:2503.04512. arxiv:2503.04512"},{"key":"e_1_2_1_29_1","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. https:\/\/doi.org\/10.5281\/zenodo.15694473 10.5281\/zenodo.15694473","DOI":"10.5281\/zenodo.15694473"},{"key":"e_1_2_1_30_1","unstructured":"Janine Lohse and Deepak Garg. 2024. An Iris for Expected Cost Analysis. arxiv:2406.00884."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.01.016"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-63287-8"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_36_1","volume-title":"Modular Reasoning about Separation of Concurrent Data Structures","author":"Svendsen Kasper","unstructured":"Kasper Svendsen, Lars Birkedal, and Matthew Parkinson. 2013. Modular Reasoning about Separation of Concurrent Data Structures. In Programming Languages and Systems, Matthias Felleisen and Philippa Gardner (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 169\u2013188. isbn:978-3-642-37036-6"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","unstructured":"The Rocq Development Team. 2024. The Rocq Prover. https:\/\/doi.org\/10.5281\/zenodo.11551307 10.5281\/zenodo.11551307","DOI":"10.5281\/zenodo.11551307"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704855"},{"key":"e_1_2_1_40_1","unstructured":"Noam Zilberstein Alexandra Silva and Joseph Tassarotti. 2024. Probabilistic Concurrent Reasoning in Outcome Logic: Independence Conditioning and Invariants. arxiv:2411.11662. arxiv: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":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:35Z","timestamp":1754412995000},"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"}}]}}