{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,28]],"date-time":"2026-08-28T17:02:56Z","timestamp":1787936576931,"version":"build-2784847793"},"reference-count":34,"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":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["2153916"],"award-info":[{"award-number":["2153916"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101003349"],"award-info":[{"award-number":["101003349"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Science and Engineering Research Council of Canada","award":["Discovery Grant"],"award-info":[{"award-number":["Discovery Grant"]}]}],"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 present\n                    <jats:sc>BlueBell<\/jats:sc>\n                    , a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools. Unary-style reasoning is very expressive and is powered by foundational mechanisms to reason about probabilistic behavior like\n                    <jats:italic toggle=\"yes\">independence<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">conditioning<\/jats:italic>\n                    . The relational style of reasoning, on the other hand, naturally shines when the properties of interest\n                    <jats:italic toggle=\"yes\">compare<\/jats:italic>\n                    the behavior of similar programs (e.g. when proving differential privacy) managing to avoid having to characterize the output distributions of the individual programs. So far, the two styles of reasoning have largely remained separate in the many program logics designed for the deductive verification of probabilistic programs. In\n                    <jats:sc>BlueBell<\/jats:sc>\n                    , we unify these styles of reasoning through the introduction of a new modality called \u201cjoint conditioning\u201d that can encode and illuminate the rich interaction between\n                    <jats:italic toggle=\"yes\">conditional independence<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">relational liftings<\/jats:italic>\n                    ; the two powerhouses from the two styles of reasoning.\n                  <\/jats:p>","DOI":"10.1145\/3704894","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1719-1749","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Bluebell: An Alliance of Relational Lifting and Independence for Probabilistic Reasoning"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2353-350X","authenticated-orcid":false,"given":"Jialu","family":"Bao","sequence":"first","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9179-5827","authenticated-orcid":false,"given":"Emanuele","family":"D'Osualdo","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarbr\u00fccken, Germany"},{"name":"University of Konstanz, Konstanz, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9005-2653","authenticated-orcid":false,"given":"Azadeh","family":"Farzan","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"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.1145\/3110265"},{"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.1109\/LICS52264.2021.9470712"},{"key":"e_1_3_2_5_1","doi-asserted-by":"crossref","unstructured":"Jialu Bao Emanuele D\u2019osualdo and Azadeh Farzan. 2024. BlueBell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning. arXiv:2402.18708","DOI":"10.1145\/3704894"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498719"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_5"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_27"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371123"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103670"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2005.11.059"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563298"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/S11225-010-9232-Z"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632868"},{"key":"e_1_3_2_17_1","unstructured":"Justin Hsu. 2017. Probabilistic couplings for probabilistic reasoning. Ph. D. Dissertation."},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_2_19_1","unstructured":"Benjamin Lucien Kaminski. 2019. Advanced weakest precondition calculi for probabilistic programs. Ph. D. Dissertation. RWTH Aachen University."},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808758"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591226"},{"key":"e_1_3_2_24_1","unstructured":"John M. Li Amal Ahmed and Steven Holtzen. 2023b. Lilac: A Modal Separation Logic for Conditional Probability. arXiv:2304.01339v2"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3661814.3662135"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563341"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","unstructured":"Carroll Morgan Annabelle McIver and Karen Seidel. 1996. Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems (1996). https:\/\/doi.org\/10.1145\/229542.229547 10.1145\/229542.229547","DOI":"10.1145\/229542.229547"},{"key":"e_1_3_2_28_1","unstructured":"Lyle Harold Ramshaw. 1979. Formalizing the analysis of algorithms. Vol. 75. Xerox Palo Alto Research Center."},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2015.12.021"},{"issue":"1","key":"e_1_3_2_30_1","first-page":"303","article-title":"Intuitionistic reasoning about Shared mutable data Structure","volume":"2","author":"Reynolds John","year":"2000","unstructured":"John Reynolds. 2000. Intuitionistic reasoning about Shared mutable data Structure. Millennial perspectives in computer science 2, 1 (2000), 303-321.","journal-title":"Millennial perspectives in computer science"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108770750.003"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_3_2_33_1","first-page":"36","article-title":"Various techniques used in connection with random digits","author":"Neumann John von","year":"1951","unstructured":"John von Neumann. 1951. Various techniques used in connection with random digits. Journal of Research of the National Bureau of Standards, Applied Math Series (1951), 36-38.","journal-title":"Journal of Research of the National Bureau of Standards, Applied Math Series"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314619"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009884"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704894","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704894","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:15:48Z","timestamp":1770200148000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704894"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":34,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704894"],"URL":"https:\/\/doi.org\/10.1145\/3704894","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"}}]}}