{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:34:13Z","timestamp":1767929653710,"version":"3.49.0"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2023,5,17]],"date-time":"2023-05-17T00:00:00Z","timestamp":1684281600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ANID FONDECYT","award":["11181208, 1190058, 3200583"],"award-info":[{"award-number":["11181208, 1190058, 3200583"]}]},{"name":"ANID Millennium Science Initiative Program code","award":["ICN17_002"],"award-info":[{"award-number":["ICN17_002"]}]},{"name":"NSF","award":["CCF-2119939"],"award-info":[{"award-number":["CCF-2119939"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2023,6,30]]},"abstract":"<jats:p>\n            Language support for differentially private programming is both crucial and delicate. While elaborate program logics can be very expressive, type-system-based approaches using linear types tend to be more lightweight and amenable to automatic checking and inference, and in particular in the presence of higher-order programming. Since the seminal design of\n            <jats:sc>Fuzz<\/jats:sc>\n            , which is restricted to \u03f5-differential privacy in its original design, significant progress has been made to support more advanced variants of differential privacy, like (\u03f5,\n            <jats:italic>\u03b4<\/jats:italic>\n            )-differential privacy. However, supporting these advanced privacy variants while also supporting higher-order programming in full has proven to be challenging. We present\n            <jats:sc>Jazz<\/jats:sc>\n            , a language and type system that uses linear types and latent contextual effects to support both advanced variants of differential privacy and higher-order programming. Latent contextual effects allow delaying the payment of effects for connectives such as products, sums, and functions, yielding advantages in terms of precision of the analysis and annotation burden upon elimination, as well as modularity. We formalize the core of\n            <jats:sc>Jazz<\/jats:sc>\n            , prove it sound for privacy via a logical relation for metric preservation, and illustrate its expressive power through a number of case studies drawn from the recent differential privacy literature.\n          <\/jats:p>","DOI":"10.1145\/3589207","type":"journal-article","created":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T11:20:48Z","timestamp":1680780048000},"page":"1-69","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Contextual Linear Types for Differential Privacy"],"prefix":"10.1145","volume":"45","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5315-0198","authenticated-orcid":false,"given":"Mat\u00edas","family":"Toro","sequence":"first","affiliation":[{"name":"Computer Science Department (DCC), University of Chile, Santiago, Chile"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2314-0287","authenticated-orcid":false,"given":"David","family":"Darais","sequence":"additional","affiliation":[{"name":"Galois, Inc., Portland, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1860-2360","authenticated-orcid":false,"given":"Chike","family":"Abuah","sequence":"additional","affiliation":[{"name":"Amazon, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3203-3742","authenticated-orcid":false,"given":"Joseph P.","family":"Near","sequence":"additional","affiliation":[{"name":"Computer Science Department, University of Vermont, Burlington, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2780-2863","authenticated-orcid":false,"given":"Dami\u00e1n","family":"\u00c1rquez","sequence":"additional","affiliation":[{"name":"Computer Science Department (DCC), University of Chile &amp; IMFD, Santiago, Chile"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0217-6483","authenticated-orcid":false,"given":"Federico","family":"Olmedo","sequence":"additional","affiliation":[{"name":"Computer Science Department (DCC), University of Chile &amp; IMFD, Santiago, Chile"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7359-890X","authenticated-orcid":false,"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"Computer Science Department (DCC), University of Chile &amp; IMFD, Santiago, Chile"}]}],"member":"320","published-online":{"date-parts":[[2023,5,17]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/1953048.2078195"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978318"},{"key":"e_1_3_3_4_2","unstructured":"Amal Ahmed. 2004. Semantics of Types for Mutable State . Ph.D. Dissertation. Princeton University."},{"key":"e_1_3_3_5_2","first-page":"69","volume-title":"Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27\u201328, 2006, Proceedings (Lecture Notes in Computer Science)","volume":"3924","author":"Ahmed Amal","year":"2006","unstructured":"Amal Ahmed. 2006. Step-indexed syntactic logical relations for recursive and quantified types. In Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27\u201328, 2006, Proceedings (Lecture Notes in Computer Science), Vol. 3924. Springer, 69\u201383."},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158146"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_3_8_2","first-page":"394","volume-title":"Proceedings of the International Conference on Machine Learning","author":"Balle Borja","year":"2018","unstructured":"Borja Balle and Yu-Xiang Wang. 2018. Improving the Gaussian mechanism for differential privacy: Analytical calibration and optimal denoising. In Proceedings of the International Conference on Machine Learning. PMLR, 394\u2013403."},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485516"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394796"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434289"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2013.26"},{"issue":"4","key":"e_1_3_3_13_2","article-title":"Relational \u22c6\u22c6\\star-liftings for differential privacy","volume":"15","author":"Barthe Gilles","year":"2019","unstructured":"Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, and Pierre-Yves Strub. 2019. Relational \u22c6\u22c6\\star-liftings for differential privacy. Logic. Meth. Comput. Sci. 15, 4 (2019). Retrieved from https:\/\/lmcs.episciences.org\/5989.","journal-title":"Logic. Meth. Comput. Sci."},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2014.36"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677000"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103670"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/2492061"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2014.56"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243863"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3188745.3188946"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53641-4_24"},{"key":"e_1_3_3_23_2","volume-title":"Proceedings of the Annual Conference on Neural Information Processing Systems (NeurIPS\u201920)","author":"Canonne Cl\u00e9ment L.","year":"2020","unstructured":"Cl\u00e9ment L. Canonne, Gautam Kamath, and Thomas Steinke. 2020. The discrete Gaussian for differential privacy. In Proceedings of the Annual Conference on Neural Information Processing Systems (NeurIPS\u201920)."},{"key":"e_1_3_3_24_2","first-page":"2652","volume-title":"Proceedings of the Conference on Advances in Neural Information Processing Systems","author":"Chaudhuri Kamalika","year":"2013","unstructured":"Kamalika Chaudhuri and Staal A. Vinterbo. 2013. A stability-based validation procedure for differentially private machine learning. In Proceedings of the Conference on Advances in Neural Information Processing Systems. 2652\u20132660."},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314603"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.5555\/1891823.1891830"},{"key":"e_1_3_3_27_2","article-title":"Really natural linear indexed type checking","volume":"1503","author":"de Amorim Arthur Azevedo","year":"2015","unstructured":"Arthur Azevedo de Amorim, Emilio Jes\u00fas Gallego Arias, Marco Gaboardi, and Justin Hsu. 2015. Really natural linear indexed type checking. CoRR abs\/1503.04522 (2015).","journal-title":"CoRR"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/2746325.2746335"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009890"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.5555\/3470152.3470192"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243818"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/1536414.1536467"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1561\/0400000042"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/2364506.2364522"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_3_3_36_2","article-title":"A programming framework for OpenDP","author":"Gaboardi Marco","year":"2020","unstructured":"Marco Gaboardi, Michael Hay, and Salil Vadhan. 2020. A programming framework for OpenDP. 6th Workshop on the Theory and Practice of Differential Privacy (TPDP\u201920). https:\/\/salil.seas.harvard.edu\/publications\/programming-framework-opendp.","journal-title":"6th Workshop on the Theory and Practice of Differential Privacy (TPDP\u201920)"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/319838.319848"},{"key":"e_1_3_3_38_2","volume-title":"A Lifetime Analysis for Higher-order Languages","author":"Hannan J.","year":"1997","unstructured":"J. Hannan, P. Hicks, and D. Liben-Nowell. 1997. A Lifetime Analysis for Higher-order Languages. Technical Report. Pennsylvania State University."},{"key":"e_1_3_3_39_2","first-page":"2339","volume-title":"Proceedings of the Conference on Advances in Neural Information Processing Systems","author":"Hardt Moritz","year":"2012","unstructured":"Moritz Hardt, Katrina Ligett, and Frank McSherry. 2012. A simple and practical algorithm for differentially private data release. In Proceedings of the Conference on Advances in Neural Information Processing Systems. 2339\u20132347."},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54415-1_71"},{"key":"e_1_3_3_41_2","volume-title":"Polymorphic Typing of an Algorithmic Language","author":"Leroy Xavier","year":"1992","unstructured":"Xavier Leroy. 1992. Polymorphic Typing of an Algorithmic Language. Technical Report Research Report 1778. INRIA."},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.14778\/3055330.3055331"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/1559845.1559850"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382264"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.11"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360598"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785668"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_47"},{"key":"e_1_3_3_53_2","first-page":"3025","volume-title":"Proceedings of the Conference on Advances in Neural Information Processing Systems","author":"Talwar Kunal","year":"2015","unstructured":"Kunal Talwar, Abhradeep Guha Thakurta, and Li Zhang. 2015. Nearly optimal private lasso. In Proceedings of the Conference on Advances in Neural Information Processing Systems. 3025\u20133033."},{"key":"e_1_3_3_54_2","article-title":"Differentially private learning with adaptive clipping","author":"Thakkar Om","year":"2019","unstructured":"Om Thakkar, Galen Andrew, and H. Brendan McMahan. 2019. Differentially private learning with adaptive clipping. arXiv preprint arXiv:1905.03871 (2019).","journal-title":"arXiv preprint arXiv:1905.03871"},{"key":"e_1_3_3_55_2","volume-title":"Contextual Linear Types for Differential Privacy \u2014 Extended with Proofs","author":"Toro Mat\u00edas","year":"2023","unstructured":"Mat\u00edas Toro, David Darais, Chike Abuah, Joseph P. Near, Dami\u00e1n \u00c1rquez, Federico Olmedo, and \u00c9ric Tanter. 2023. Contextual Linear Types for Differential Privacy \u2014 Extended with Proofs. Technical Report TR\/DCC-2023-1. University of Chile."},{"key":"e_1_3_3_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314619"},{"issue":"2","key":"e_1_3_3_57_2","article-title":"Differentially private SQL with bounded user contribution","volume":"2020","author":"Wilson Royce J.","year":"2020","unstructured":"Royce J. Wilson, Celia Yuxing Zhang, William Lam, Damien Desfontaines, Daniel Simmons-Marengo, and Bryant Gipson. 2020. Differentially private SQL with bounded user contribution. Proc. Privac. Enhanc. Technol. 2020, 2 (2020).","journal-title":"Proc. Privac. Enhanc. Technol."},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3064047"},{"key":"e_1_3_3_59_2","article-title":"Opacus: User-friendly differential privacy library in PyTorch","author":"Yousefpour Ashkan","year":"2021","unstructured":"Ashkan Yousefpour, Igor Shilov, Alexandre Sablayrolles, Davide Testuggine, Karthik Prasad, Mani Malek, John Nguyen, Sayan Ghosh, Akash Bharadwaj, Jessica Zhao, et al. 2021. Opacus: User-friendly differential privacy library in PyTorch. arXiv preprint arXiv:2109.12298 (2021).","journal-title":"arXiv preprint arXiv:2109.12298"},{"key":"e_1_3_3_60_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009884"},{"key":"e_1_3_3_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341697"},{"key":"e_1_3_3_62_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3428233","article-title":"Testing differential privacy with dual interpreters","volume":"4","author":"Zhang Hengchu","year":"2020","unstructured":"Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. Pierce, and Aaron Roth. 2020. Testing differential privacy with dual interpreters. Proc. ACM Program. Lang. 4, OOPSLA (2020), 1\u201326.","journal-title":"Proc. ACM Program. Lang."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3589207","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3589207","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:48:53Z","timestamp":1750182533000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3589207"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,17]]},"references-count":61,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,6,30]]}},"alternative-id":["10.1145\/3589207"],"URL":"https:\/\/doi.org\/10.1145\/3589207","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,5,17]]},"assertion":[{"value":"2021-02-22","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-02-25","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-05-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}