{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,14]],"date-time":"2026-04-14T22:25:58Z","timestamp":1776205558834,"version":"3.50.1"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-2220408"],"award-info":[{"award-number":["CCF-2220408"]}],"id":[{"id":"10.13039\/100000001","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":[[2023,6,6]]},"abstract":"<jats:p>We present Lilac, a separation logic for reasoning about probabilistic programs where separating conjunction captures probabilistic independence. Inspired by an analogy with mutable state where sampling corresponds to dynamic allocation, we show how probability spaces over a fixed, ambient sample space appear to be the natural analogue of heap fragments, and present a new combining operation on them such that probability spaces behave like heaps and measurability of random variables behaves like ownership. This combining operation forms the basis for our model of separation, and produces a logic with many pleasant properties. In particular, Lilac has a frame rule identical to the ordinary one, and naturally accommodates advanced features like continuous random variables and reasoning about quantitative properties of programs. Then we propose a new modality based on disintegration theory for reasoning about conditional probability. We show how the resulting modal logic validates examples from prior work, and give a formal verification of an intricate weighted sampling algorithm whose correctness depends crucially on conditional independence structure.<\/jats:p>","DOI":"10.1145\/3591226","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"148-171","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["Lilac: A Modal Separation Logic for Conditional Probability"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2130-5092","authenticated-orcid":false,"given":"John M.","family":"Li","sequence":"first","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7424-572X","authenticated-orcid":false,"given":"Amal","family":"Ahmed","sequence":"additional","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8190-5412","authenticated-orcid":false,"given":"Steven","family":"Holtzen","sequence":"additional","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470712"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498719"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_5"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371123"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275499"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_18"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1111\/1467-9574.00056"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_14"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338112"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2005.11.003"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1137\/1119053"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2020.107239"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004858"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192400"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-010-9232-z"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2013.11.004"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068402001412"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005137"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_27"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61871-1"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43425-4_14"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808758"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009855"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/UPO9781844653621.010"},{"key":"e_1_2_1_28_1","volume-title":"Introduction to embedded systems: A cyber-physical systems approach","author":"Lee Edward Ashford","unstructured":"Edward Ashford Lee and Sanjit Arunkumar Seshia . 2016. Introduction to embedded systems: A cyber-physical systems approach . Mit Press . https:\/\/doi.org\/10.5555\/3086978 10.5555\/3086978 Edward Ashford Lee and Sanjit Arunkumar Seshia. 2016. Introduction to embedded systems: A cyber-physical systems approach. Mit Press. https:\/\/doi.org\/10.5555\/3086978"},{"key":"#cr-split#-e_1_2_1_29_1.1","unstructured":"John M Li Amal Ahmed and Steven Holtzen. 2023. Lilac: a Modal Separation Logic for Conditional Probability. arXiv preprint arXiv:2304.01339 https:\/\/doi.org\/10.48550\/arXiv.2304.01339 10.48550\/arXiv.2304.01339"},{"key":"#cr-split#-e_1_2_1_29_1.2","unstructured":"John M Li Amal Ahmed and Steven Holtzen. 2023. Lilac: a Modal Separation Logic for Conditional Probability. arXiv preprint arXiv:2304.01339 https:\/\/doi.org\/10.48550\/arXiv.2304.01339"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-028-4-286"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1498926.1498929"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-58603-976-9-285"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009852"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314639"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/b98956"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_32"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108770750.003"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935313"},{"key":"e_1_2_1_42_1","volume-title":"Structural foundations for probabilistic programming languages","author":"Stein Dario Maximilian","unstructured":"Dario Maximilian Stein . 2021. Structural foundations for probabilistic programming languages . University of Oxford. Dario Maximilian Stein. 2021. Structural foundations for probabilistic programming languages. University of Oxford."},{"key":"e_1_2_1_43_1","unstructured":"Terence Tao. 2015. 254A notes 0: A review of probability theory. https:\/\/terrytao.wordpress.com\/2010\/01\/01\/254a-notes-0-a-review-of-probability-theory\/ \t\t\t\t  Terence Tao. 2015. 254A notes 0: A review of probability theory. https:\/\/terrytao.wordpress.com\/2010\/01\/01\/254a-notes-0-a-review-of-probability-theory\/"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236782"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498677"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470673"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591226","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591226","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:46Z","timestamp":1750178866000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591226"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":48,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591226"],"URL":"https:\/\/doi.org\/10.1145\/3591226","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}