{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T21:36:38Z","timestamp":1790112998056,"version":"4.0.1"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T00:00:00Z","timestamp":1780876800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/legalcode"}],"funder":[{"name":"National Science Foundation","award":["NSF2338317"],"award-info":[{"award-number":["NSF2338317"]}]},{"name":"Carlsberg Foundation","award":["CF23-0791"],"award-info":[{"award-number":["CF23-0791"]}],"id":[{"id":"https:\/\/ror.org\/01kpjmx04","id-type":"ROR","asserted-by":"crossref"}]},{"name":"Villum","award":["VIL25804"],"award-info":[{"award-number":["VIL25804"]}]},{"name":"Villum","award":["VIL73403"],"award-info":[{"award-number":["VIL73403"]}]},{"name":"European Research Council","award":["ERC101096090"],"award-info":[{"award-number":["ERC101096090"]}],"id":[{"id":"https:\/\/ror.org\/0472cxd90","id-type":"ROR","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,6,8]]},"abstract":"<jats:p>Differential privacy is the standard method for privacy-preserving data analysis. The importance of having strong guarantees on the reliability of implementations of differentially private algorithms is widely recognized and has sparked fruitful research on formal methods. However, the design patterns and language features used in modern DP libraries as well as the classes of guarantees that the library designers wish to establish often fall outside of the scope of previous verification approaches.<\/jats:p>\n                  <jats:p>We introduce a program logic suitable for verifying differentially private implementations written in complex, general-purpose programming languages. Our logic has first-class support for reasoning about privacy budgets as a separation logic resource. The expressiveness of the logic and the target language allow our approach to handle common programming patterns used in the implementation of libraries for differential privacy, such as privacy filters and caching. While previous work has focused on developing guarantees for programs written in domain-specific languages or for privacy mechanisms in isolation, our logic can reason modularly about primitives, higher-order combinators, and interactive algorithms.<\/jats:p>\n                  <jats:p>We demonstrate the applicability of our approach by implementing a verified library of differential privacy mechanisms, including an online version of the Sparse Vector Technique, as well as a privacy filter inspired by the popular Python library OpenDP, which crucially relies on our ability to handle the combination of randomization, local state, and higher-order functions. We demonstrate that our specifications are general and reusable by instantiating them to verify clients of our library. All of our results have been foundationally verified in the Rocq Prover.<\/jats:p>","DOI":"10.1145\/3808311","type":"journal-article","created":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T18:04:09Z","timestamp":1780941849000},"page":"1610-1634","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0198-7751","authenticated-orcid":false,"given":"Philipp G.","family":"Haselwarter","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-0002-4124-5720","authenticated-orcid":false,"given":"Kwing Hei","family":"Li","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"},{"name":"Amazon Web Services, 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":[[2026,6,8]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978318"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Chik\u00e9 Abuah David Darais and Joseph P. Near . 2022. Solo: A Lightweight Static Analysis for Differential Privacy. Proc. ACM Program. Lang. https:\/\/doi.org\/10.1145\/3563313 10.1145\/3563313","DOI":"10.1145\/3563313"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Alejandro Aguirre Gilles Barthe Marco Gaboardi Deepak Garg Shin-ya Katsumata and Tetsuya Sato . 2021. Higherorder probabilistic adversarial computations: categorical semantics and program logics. Proc. ACM Program. Lang. https:\/\/doi.org\/10.1145\/3473598 10.1145\/3473598","DOI":"10.1145\/3473598"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","unstructured":"Alejandro Aguirre Philipp G. Haselwarter Markus de Medeiros Kwing Hei Li Simon Oddershede Gregersen Joseph Tassarotti and Lars Birkedal . 2024. Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs. Proc. ACM Program. Lang. https:\/\/doi.org\/10.1145\/3674635 10.1145\/3674635","DOI":"10.1145\/3674635"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158146"},{"key":"e_1_3_2_7_2","first-page":"6280","volume-title":"Proceedings of the 32nd International Conference on Neural Information Processing Systems","author":"Balle Borja","year":"2018","unstructured":"Borja Balle , Gilles Barthe , and Marco Gaboardi . 2018. Privacy amplification by subsampling: tight analyses via couplings and divergences. In Proceedings of the 32nd International Conference on Neural Information Processing Systems (Montr\u00e9al, Canada) (NIPS\u201918). USA, 6280\u20136290."},{"key":"e_1_3_2_8_2","doi-asserted-by":"crossref","unstructured":"Jialu Bao Emanuele D\u2019Osualdo and Azadeh Farzan . 2025. Bluebell: An Alliance of Relational Lifting and Independence for Probabilistic Reasoning. Proc. ACM Program. Lang.","DOI":"10.1145\/3704894"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_27"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978391"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677000"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103670"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.5555\/3495724.3497039"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1017\/9781108770750.008"},{"key":"e_1_3_2_16_2","volume-title":"Hands-on Differential Privacy: Introduction to the Theory and Practice Using OpenDP (first edition ed.)","author":"Cowan Ethan","year":"2024","unstructured":"Ethan Cowan , Michael Shoemate , and Mayana Pereira . 2024. Hands-on Differential Privacy: Introduction to the Theory and Practice Using OpenDP (first edition ed.). O\u2019Reilly Media, Inc, Sebastopol, CA."},{"key":"e_1_3_2_17_2","first-page":"1","volume-title":"Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201819)","author":"Amorim Arthur Azevedo de","year":"2021","unstructured":"Arthur Azevedo de Amorim , Marco Gaboardi , Justin Hsu , and Shin-ya Katsumata . 2021. Probabilistic Relational Reasoning via Metrics. In Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201819). Canada, 1\u201319."},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3729294"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/11681878_14"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1561\/0400000042"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs17(3:9)2021"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1137\/09076828X"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Simon Oddershede Gregersen Alejandro Aguirre Philipp G. Haselwarter Joseph Tassarotti and Lars Birkedal . 2024. Almost-Sure Termination by Guarded Refinement. Proc. ACM Program. Lang. https:\/\/doi.org\/10.1145\/3674632 10.1145\/3674632","DOI":"10.1145\/3674632"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632868"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.19089094"},{"key":"e_1_3_2_27_2","doi-asserted-by":"crossref","unstructured":"Philipp G. Haselwarter Alejandro Aguirre Simon Oddershede Gregersen Kwing Hei Li Joseph Tassarotti and Lars Birkedal . 2026. Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version). arXiv:2604.12713 [cs.PL] https:\/\/arxiv.org\/abs\/2604.12713","DOI":"10.1145\/3808311"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Philipp G. Haselwarter Kwing Hei Li Alejandro Aguirre Simon Oddershede Gregersen Joseph Tassarotti and Lars Birkedal . 2025. Approximate Relational Reasoning for Higher-Order Probabilistic Programs. Proc. ACM Program. Lang. https:\/\/doi.org\/10.1145\/3704877 10.1145\/3704877","DOI":"10.1145\/3704877"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","unstructured":"Philipp G. Haselwarter Kwing Hei Li Markus de Medeiros Simon Oddershede Gregersen Alejandro Aguirre Joseph Tassarotti and Lars Birkedal . 2024. Tachis: Higher-Order Separation Logic with Credits for Expected Costs. Proc. ACM Program. Lang. https:\/\/doi.org\/10.1145\/3689753 10.1145\/3689753","DOI":"10.1145\/3689753"},{"key":"e_1_3_2_30_2","volume-title":"Probabilistic Couplings for Probabilistic Reasoning. Ph. D. Dissertation","author":"Hsu Justin","year":"2017","unstructured":"Justin Hsu . 2017. Probabilistic Couplings for Probabilistic Reasoning. Ph. D. Dissertation. University of Pennsylvania. arXiv:1710.09951."},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jspi.2004.08.014"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613174"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.14778\/3342263.3342274"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","unstructured":"Elisabet Lobo-Vesga Alejandro Russo and Marco Gaboardi . 2020. A Programming Framework for Differential Privacy with Accuracy Concentration Bounds. In 2020 IEEE Symposium on Security and Privacy (SP). 411\u2013428. https:\/\/doi.org\/10.1109\/SP40000.2020.00086 10.1109\/SP40000.2020.00086","DOI":"10.1109\/SP40000.2020.00086"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689726"},{"key":"e_1_3_2_37_2","unstructured":"Janine Lohse and Deepak Garg . 2024. An Iris for Expected Cost Analysis. arXiv:2406.00884 [cs.PL]"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.14778\/3055330.3055331"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"Rupak Majumdar and V.R. Sathiyanarayana . 2025. Sound and Complete Proof Rules for Probabilistic Termination. Proc. ACM Program. Lang. https:\/\/doi.org\/10.1145\/3704899 10.1145\/3704899","DOI":"10.1145\/3704899"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.14778\/3574245.3574246"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382264"},{"key":"e_1_3_2_42_2","unstructured":"Joseph P. Near and Chik\u00e9 Abuah . 2021. Programming Differential Privacy. Vol. 1 https:\/\/programming-dp.com\/"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"Joseph P. Near David Darais Chike Abuah Tim Stevens Pranav Gaddamadugu Lun Wang Neel Somani Mu Zhang Nikhil Sharma Alex Shan and Dawn Song . 2019. Duet: An Expressive Higher-Order Language and Linear Type System for Statically Enforcing Differential Privacy. Proc. ACM Program. Lang. https:\/\/doi.org\/10.1145\/3360598 10.1145\/3360598","DOI":"10.1145\/3360598"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"Shangfu Peng Yin Yang Zhenjie Zhang Marianne Winslett and Yong Yu . 2013. Query Optimization for Differentially Private Data Management Systems. In 2013 IEEE 29th International Conference on Data Engineering (ICDE). 1093\u20131104. https:\/\/doi.org\/10.1109\/ICDE.2013.6544900 10.1109\/ICDE.2013.6544900","DOI":"10.1109\/ICDE.2013.6544900"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_3_2_46_2","volume-title":"Advances in Neural Information Processing Systems","author":"Rogers Ryan M","year":"2016","unstructured":"Ryan M Rogers , Aaron Roth , Jonathan Ullman , and Salil Vadhan . 2016. Privacy Odometers and Filters: Pay-as-you-Go Composition. In Advances in Neural Information Processing Systems. Vol. 29. Curran Associates, Inc."},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","unstructured":"Tetsuya Sato . 2016. Approximate Relational Hoare Logic for Continuous Random Samplings. In The Thirty-second Conference on the Mathematical Foundations of Programming Semantics MFPS 2016. 2016.09.043. https:\/\/doi.org\/10.1016\/J.ENTCS 10.1016\/J.ENTCS","DOI":"10.1016\/J.ENTCS"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","unstructured":"Tetsuya Sato Gilles Barthe Marco Gaboardi Justin Hsu and Shin-ya Katsumata . 2019. Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy. In 2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1\u201314. https:\/\/doi.org\/10.1109\/LICS.2019.8785668 10.1109\/LICS.2019.8785668","DOI":"10.1109\/LICS.2019.8785668"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3703595.3705875"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3589207"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","unstructured":"Daniel Winograd-Cort Andreas Haeberlen Aaron Roth and Benjamin C. Pierce . 2017. A Framework for Adaptive Differential Privacy. Proc. ACM Program. Lang. 10:1\u201310:29. https:\/\/doi.org\/10.1145\/3110254 10.1145\/3110254","DOI":"10.1145\/3110254"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009884"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341697"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808311","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808311","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T10:48:25Z","timestamp":1790074105000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3808311"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,8]]},"references-count":52,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2026,6,8]]}},"alternative-id":["10.1145\/3808311"],"URL":"https:\/\/doi.org\/10.1145\/3808311","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,8]]},"assertion":[{"value":"2025-11-13","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-06-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}