{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T02:26:08Z","timestamp":1784255168786,"version":"3.55.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"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":["2035314,1943130,2040249,2040222,2152831"],"award-info":[{"award-number":["2035314,1943130,2040249,2040222,2152831"]}],"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":[[2022,1,16]]},"abstract":"<jats:p>\n            Formal reasoning about hashing-based probabilistic data structures often requires reasoning about random variables where when one variable gets larger (such as the number of elements hashed into one bucket), the others tend to be smaller (like the number of elements hashed into the other buckets). This is an example of\n            <jats:italic>negative dependence<\/jats:italic>\n            , a generalization of probabilistic independence that has recently found interesting applications in algorithm design and machine learning. Despite the usefulness of negative dependence for the analyses of probabilistic data structures, existing verification methods cannot establish this property for randomized programs.\n          <\/jats:p>\n          <jats:p>\n            To fill this gap, we design LINA, a probabilistic separation logic for reasoning about negative dependence. Following recent works on probabilistic separation logic using\n            <jats:italic>separating conjunction<\/jats:italic>\n            to reason about the probabilistic independence of random variables, we use separating conjunction to reason about negative dependence. Our assertion logic features two separating conjunctions, one for independence and one for negative dependence. We generalize the logic of bunched implications (BI) to support multiple separating conjunctions, and provide a sound and complete proof system. Notably, the semantics for separating conjunction relies on a\n            <jats:italic>non-deterministic<\/jats:italic>\n            , rather than partial, operation for combining resources. By drawing on closure properties for negative dependence, our program logic supports a Frame-like rule for negative dependence and\n            <jats:italic>monotone<\/jats:italic>\n            operations. We demonstrate how LINA can verify probabilistic properties of hash-based data structures and balls-into-bins processes.\n          <\/jats:p>","DOI":"10.1145\/3498719","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["A separation logic for negative dependence"],"prefix":"10.1145","volume":"6","author":[{"given":"Jialu","family":"Bao","sequence":"first","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marco","family":"Gaboardi","sequence":"additional","affiliation":[{"name":"Boston University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joseph","family":"Tassarotti","sequence":"additional","affiliation":[{"name":"Boston College, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Conference on Computational Learning Theory (COLT). 49, Proceedings of Machine Learning Research","author":"Anari Nima","year":"2016","unstructured":"Nima Anari , Shayan Oveis Gharan , and Alireza Rezaei . 2016 . Monte Carlo Markov chain algorithms for sampling Strongly Rayleigh distributions and determinantal point processes . In Conference on Computational Learning Theory (COLT). 49, Proceedings of Machine Learning Research , New York, New York. 103\u2013115. http:\/\/proceedings.mlr.press\/v49\/anari16.html Nima Anari, Shayan Oveis Gharan, and Alireza Rezaei. 2016. Monte Carlo Markov chain algorithms for sampling Strongly Rayleigh distributions and determinantal point processes. In Conference on Computational Learning Theory (COLT). 49, Proceedings of Machine Learning Research, New York, New York. 103\u2013115. http:\/\/proceedings.mlr.press\/v49\/anari16.html"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470712"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498719"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31113-0_1"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371123"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-017-0320-4"},{"key":"e_1_2_2_8_1","volume-title":"Bercea and Guy Even","author":"Ioana","year":"2019","unstructured":"Ioana O. Bercea and Guy Even . 2019 . Fully-dynamic space-efficient dictionaries and filters with constant number of memory accesses. CoRR , abs\/1911.05060 (2019), arxiv:1911.05060 Ioana O. Bercea and Guy Even. 2019. Fully-dynamic space-efficient dictionaries and filters with constant number of memory accesses. CoRR, abs\/1911.05060 (2019), arxiv:1911.05060"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/362686.362692"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0894-0347-08-00618-8"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2008.05.018"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1467-9469.2011.00766.x"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.14778\/1938545.1938550"},{"key":"e_1_2_2_16_1","volume-title":"Bunched logics: a uniform approach. Ph. D. Dissertation","author":"Docherty Simon","unstructured":"Simon Docherty . 2019. Bunched logics: a uniform approach. Ph. D. Dissertation . UCL (University College London) . Simon Docherty. 2019. Bunched logics: a uniform approach. Ph. D. Dissertation. UCL (University College London)."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0963548306007772"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/299633.299634"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_16"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1214\/aos\/1176346079"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1561\/2200000044"},{"key":"e_1_2_2_26_1","volume-title":"Probability and computing - randomized algorithms and probabilistic analysis","author":"Mitzenmacher Michael","unstructured":"Michael Mitzenmacher and Eli Upfal . 2005. Probability and computing - randomized algorithms and probabilistic analysis . Cambridge University Press . Michael Mitzenmacher and Eli Upfal. 2005. Probability and computing - randomized algorithms and probabilistic analysis. Cambridge University Press."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_2_28_1","volume-title":"Pym","author":"O\u2019Hearn Peter W.","year":"1999","unstructured":"Peter W. O\u2019Hearn and David J . Pym . 1999 . The logic of bunched implications. Bulletin of Symbolic Logic , 215\u2013244. https:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.27.4742&rep=rep1&type=pdf Peter W. O\u2019Hearn and David J. Pym. 1999. The logic of bunched implications. Bulletin of Symbolic Logic, 215\u2013244. https:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.27.4742&rep=rep1&type=pdf"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_24"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.533200"},{"key":"e_1_2_2_32_1","unstructured":"David J. Pym. 2002. The semantics and proof theory of the logic of Bunched implications (Applied Logic Series Vol. 26). Kluwer Academic Publishers. Errata and Remarks maintained at: http:\/\/www.cantab.net\/users\/david.pym\/BI-monograph-errata.pdf  David J. Pym. 2002. The semantics and proof theory of the logic of Bunched implications (Applied Logic Series Vol. 26). Kluwer Academic Publishers. Errata and Remarks maintained at: http:\/\/www.cantab.net\/users\/david.pym\/BI-monograph-errata.pdf"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.11.020"},{"key":"e_1_2_2_34_1","first-page":"303","article-title":"Intuitionistic reasoning about shared mutable data structure","volume":"2","author":"Reynolds John C.","year":"2001","unstructured":"John C. Reynolds . 2001 . Intuitionistic reasoning about shared mutable data structure . Millennial Perspectives in Computer Science , 2 , 1 (2001), 303 \u2013 321 . https:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.11.5999&rep=rep1&type=pdf John C. Reynolds. 2001. Intuitionistic reasoning about shared mutable data structure. Millennial Perspectives in Computer Science, 2, 1 (2001), 303\u2013321. https:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.11.5999&rep=rep1&type=pdf","journal-title":"Millennial Perspectives in Computer Science"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737964"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.2001.959935"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454102"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498719","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498719","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498719","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:29Z","timestamp":1750188629000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498719"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":38,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498719"],"URL":"https:\/\/doi.org\/10.1145\/3498719","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}