{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:19Z","timestamp":1780994539104,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,7,8]],"date-time":"2024-07-08T00:00:00Z","timestamp":1720396800000},"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"}]},{"DOI":"10.13039\/100006168","name":"National Nuclear Security Administration","doi-asserted-by":"publisher","award":["DE-NA0003525"],"award-info":[{"award-number":["DE-NA0003525"]}],"id":[{"id":"10.13039\/100006168","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,7,8]]},"DOI":"10.1145\/3661814.3662135","type":"proceedings-article","created":{"date-parts":[[2024,6,21]],"date-time":"2024-06-21T12:30:12Z","timestamp":1718973012000},"page":"1-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["A Nominal Approach to Probabilistic Separation Logic"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2130-5092","authenticated-orcid":false,"given":"John M.","family":"Li","sequence":"first","affiliation":[{"name":"Computer Science, Northeastern University, Boston, MA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9734-5747","authenticated-orcid":false,"given":"Jon","family":"Aytac","sequence":"additional","affiliation":[{"name":"Sandia National Laboratories, Livermore, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5973-0671","authenticated-orcid":false,"given":"Philip","family":"Johnson-Freyd","sequence":"additional","affiliation":[{"name":"Sandia National Laboratories, Livermore, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7424-572X","authenticated-orcid":false,"given":"Amal","family":"Ahmed","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, MA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8190-5412","authenticated-orcid":false,"given":"Steven","family":"Holtzen","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, MA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,7,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473598"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470712"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498719"},{"key":"e_1_3_2_1_4_1","unstructured":"Hendrik P Barendregt et al. 1984. The lambda calculus. Vol. 3. North-Holland Amsterdam."},{"key":"e_1_3_2_1_5_1","volume-title":"Proceedings of the ACM on Programming Languages 4, POPL","author":"Barthe Gilles","year":"2019","unstructured":"Gilles Barthe, Justin Hsu, and Kevin Liao. 2019. A probabilistic separation logic. Proceedings of the ACM on Programming Languages 4, POPL (2019), 1--30."},{"key":"e_1_3_2_1_6_1","unstructured":"Bodil Biering. 2004. On the Logic of Bunched Implications and its Relation to Separation Logic. (2004)."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(83)90069-5"},{"key":"e_1_3_2_1_8_1","volume-title":"Freyd's models for the independence of the axiom of choice","author":"Blass Andreas","unstructured":"Andreas Blass and Andrej \u0160\u010dedrov. 1989. Freyd's models for the independence of the axiom of choice. Vol. 404. American Mathematical Soc."},{"key":"e_1_3_2_1_9_1","volume-title":"Applications of Sheaves: Proceedings of the Research Symposium on Applications of Sheaf Theory to Logic, Algebra, and Analysis, Durham, July 9--21","author":"Breitsprecher Siegfried","year":"2006","unstructured":"Siegfried Breitsprecher. 2006. On the concept of a measurable space I. In Applications of Sheaves: Proceedings of the Research Symposium on Applications of Sheaf Theory to Logic, Algebra, and Analysis, Durham, July 9--21, 1977. Springer, 157--168."},{"key":"e_1_3_2_1_10_1","unstructured":"Carsten Butz and Ieke Moerdijk. 1996. Representing topoi by topological groupoids. (1996)."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2015.11.050"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1111\/1467-9574.00056"},{"key":"e_1_3_2_1_13_1","volume-title":"Reports of the","author":"Day Brian","unstructured":"Brian Day. 1970. On closed categories of functors. In Reports of the Midwest Category Seminar IV. Springer, 1--38."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2874773"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0001-8708(02)00046-4"},{"key":"e_1_3_2_1_16_1","volume-title":"On the Galois theory of Grothendieck. arXiv preprint math\/0009145","author":"Dubuc Eduardo J","year":"2000","unstructured":"Eduardo J Dubuc and C Sanchez de la Vega. 2000. On the Galois theory of Grothendieck. arXiv preprint math\/0009145 (2000)."},{"key":"e_1_3_2_1_17_1","volume-title":"Measure theory","author":"Fremlin David Heaver","unstructured":"David Heaver Fremlin. 2000. Measure theory. Vol. 4. Torres Fremlin."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2020.107239"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004858"},{"key":"e_1_3_2_1_20_1","volume-title":"Categorical Aspects of Topology and Analysis: Proceedings of an International Conference Held at Carleton University","author":"Giry Michele","year":"2006","unstructured":"Michele Giry. 2006. A categorical approach to probability theory. In Categorical Aspects of Topology and Analysis: Proceedings of an International Conference Held at Carleton University, Ottawa, August 11--15, 1981. Springer, 68--85."},{"key":"e_1_3_2_1_21_1","series-title":"Lecture Notes in Mathematics","volume-title":"Rev\u00e9tements \u00c9tales et Groupe Fondamental (SGA 1)","author":"Grothendieck Alexander","unstructured":"Alexander Grothendieck. 1971. Rev\u00e9tements \u00c9tales et Groupe Fondamental (SGA 1). Lecture Notes in Mathematics, Vol. 224. Springer-Verlag."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005137"},{"key":"e_1_3_2_1_23_1","volume-title":"Model theory","author":"Hodges Wilfrid","unstructured":"Wilfrid Hodges. 1993. Model theory. Cambridge university press."},{"key":"e_1_3_2_1_24_1","volume-title":"A sheaf theoretic approach to measure theory. Ph. D. Dissertation","author":"Jackson Matthew","unstructured":"Matthew Jackson. 2006. A sheaf theoretic approach to measure theory. Ph. D. Dissertation. University of Pittsburgh."},{"key":"e_1_3_2_1_25_1","volume-title":"An extension of the Galois theory of Grothendieck","author":"Joyal Andr\u00e9","unstructured":"Andr\u00e9 Joyal and Myles Tierney. 1984. An extension of the Galois theory of Grothendieck. Vol. 309. American Mathematical Soc."},{"key":"e_1_3_2_1_26_1","volume-title":"Foundations of modern probability","author":"Kallenberg Olav","unstructured":"Olav Kallenberg. 1997. Foundations of modern probability. Vol. 2. Springer."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591226"},{"key":"e_1_3_2_1_28_1","volume-title":"Sheaves in geometry and logic: A first introduction to topos theory","author":"MacLane Saunders","unstructured":"Saunders MacLane and Ieke Moerdijk. 2012. Sheaves in geometry and logic: A first introduction to topos theory. Springer Science & Business Media."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1982-0637034-1"},{"key":"e_1_3_2_1_30_1","volume-title":"Applied categorical structures 11","author":"Menni Matias","year":"2003","unstructured":"Matias Menni. 2003. About \u1d0e-quantifiers. Applied categorical structures 11 (2003), 421--445."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.175187"},{"key":"e_1_3_2_1_32_1","volume-title":"A model for syntactic control of interference. Mathematical structures in computer science 3, 4","author":"O'Hearn Peter W.","year":"1993","unstructured":"Peter W. O'Hearn. 1993. A model for syntactic control of interference. Mathematical structures in computer science 3, 4 (1993), 435--465."},{"key":"e_1_3_2_1_33_1","volume-title":"M Takeyama, and Robert D Tennent.","author":"O'Hearn Peter W","year":"1995","unstructured":"Peter W O'Hearn, AJ Power, M Takeyama, and Robert D Tennent. 1995. Syntactic control of interference revisited. Electronic notes in Theoretical computer science 1 (1995), 447--486."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2021.106884"},{"key":"e_1_3_2_1_35_1","volume-title":"Nominal logic, a first order theory of names and binding. Information and computation 186, 2","author":"Pitts Andrew M","year":"2003","unstructured":"Andrew M Pitts. 2003. Nominal logic, a first order theory of names and binding. Information and computation 186, 2 (2003), 165--193."},{"key":"e_1_3_2_1_36_1","volume-title":"Nominal sets: Names and symmetry in computer science","author":"Pitts Andrew M","unstructured":"Andrew M Pitts. 2013. Nominal sets: Names and symmetry in computer science. Cambridge University Press."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57182-5_8"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512766"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_1_40_1","first-page":"107","article-title":"On the fundamental ideas of measure theory","volume":"25","author":"Rohlin VA","year":"1949","unstructured":"VA Rohlin. 1949. On the fundamental ideas of measure theory. Mat. Sb.(NS) 25, 67 (1949), 107--150.","journal-title":"Mat. Sb.(NS)"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434292"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290351"},{"key":"e_1_3_2_1_43_1","volume-title":"Proceedings of the ACM on Programming Languages 2, POPL","author":"\u015acibior Adam","year":"2017","unstructured":"Adam \u015acibior, Ohad Kammar, Matthijs V\u00e1k\u00e1r, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K Moss, Chris Heunen, and Zoubin Ghahramani. 2017. Denotational validation of higher-order Bayesian inference. Proceedings of the ACM on Programming Languages 2, POPL (2017), 1--29."},{"key":"e_1_3_2_1_44_1","unstructured":"Alex Simpson. 2016. Probability sheaves. https:\/\/synapse.math.univ-toulouse.fr\/index.php\/s\/QWrxKeXn31mN3gz Accessed: 2023-10-02."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CALCO.2017.1"},{"key":"e_1_3_2_1_46_1","unstructured":"Alex Simpson. 2018. Synthetic Probability Theory. (2018). http:\/\/tobiasfritz.science\/2019\/cps_workshop\/slides\/simpson.pdf Mathematics and Theoretical Computing Seminar at the University of Ljubljana."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3661814.3662132"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935313"},{"key":"e_1_3_2_1_49_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\/ Accessed: 2023-10-02."},{"key":"e_1_3_2_1_50_1","volume-title":"Proceedings of the ACM on Programming Languages 3, POPL","author":"V\u00e1k\u00e1r Matthijs","year":"2019","unstructured":"Matthijs V\u00e1k\u00e1r, Ohad Kammar, and Sam Staton. 2019. A domain theory for statistical probabilistic programming. Proceedings of the ACM on Programming Languages 3, POPL (2019), 1--29."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470673"}],"event":{"name":"LICS '24: 39th Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Tallinn Estonia","acronym":"LICS '24","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","IEEE Computer Society","EACSL"]},"container-title":["Proceedings of the 39th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3661814.3662135","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3661814.3662135","content-type":"text\/html","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3661814.3662135","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3661814.3662135","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:06:21Z","timestamp":1750291581000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3661814.3662135"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,8]]},"references-count":51,"alternative-id":["10.1145\/3661814.3662135","10.1145\/3661814"],"URL":"https:\/\/doi.org\/10.1145\/3661814.3662135","relation":{},"subject":[],"published":{"date-parts":[[2024,7,8]]},"assertion":[{"value":"2024-07-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}