{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T20:29:14Z","timestamp":1790713754024,"version":"4.1.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1901278"],"award-info":[{"award-number":["1901278"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100011039","name":"IARPA","doi-asserted-by":"crossref","award":["2019-1902070008"],"award-info":[{"award-number":["2019-1902070008"]}],"id":[{"id":"10.13039\/100011039","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"crossref","award":["N66001-15-C-4066"],"award-info":[{"award-number":["N66001-15-C-4066"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>During the past decade, differential privacy has become the gold standard for protecting the privacy of individuals. However, verifying that a particular program provides differential privacy often remains a manual task to be completed by an expert in the field. Language-based techniques have been proposed for fully automating proofs of differential privacy via type system design, however these results have lagged behind advances in differentially-private algorithms, leaving a noticeable gap in programs which can be automatically verified while also providing state-of-the-art bounds on privacy.<\/jats:p>\n          <jats:p>We propose Duet, an expressive higher-order language, linear type system and tool for automatically verifying differential privacy of general-purpose higher-order programs. In addition to general purpose programming, Duet supports encoding machine learning algorithms such as stochastic gradient descent, as well as common auxiliary data analysis tasks such as clipping, normalization and hyperparameter tuning - each of which are particularly challenging to encode in a statically verified differential privacy framework.<\/jats:p>\n          <jats:p>We present a core design of the Duet language and linear type system, and complete key proofs about privacy for well-typed programs. We then show how to extend Duet to support realistic machine learning applications and recent variants of differential privacy which result in improved accuracy for many practical differentially private algorithms. Finally, we implement several differentially private machine learning algorithms in Duet which have never before been automatically verified by a language-based tool, and we present experimental results which demonstrate the benefits of Duet's language design in terms of accuracy of trained machine learning models.<\/jats:p>","DOI":"10.1145\/3360598","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":33,"title":["Duet: an expressive higher-order language and linear type system for statically enforcing differential privacy"],"prefix":"10.1145","volume":"3","author":[{"given":"Joseph P.","family":"Near","sequence":"first","affiliation":[{"name":"University of Vermont, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Darais","sequence":"additional","affiliation":[{"name":"University of Vermont, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chike","family":"Abuah","sequence":"additional","affiliation":[{"name":"University of Vermont, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tim","family":"Stevens","sequence":"additional","affiliation":[{"name":"University of Vermont, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pranav","family":"Gaddamadugu","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lun","family":"Wang","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Neel","family":"Somani","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mu","family":"Zhang","sequence":"additional","affiliation":[{"name":"University of Utah, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nikhil","family":"Sharma","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alex","family":"Shan","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dawn","family":"Song","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"2016. Apple previews iOS 10 the biggest iOS release ever. http:\/\/www.apple.com\/newsroom\/2016\/06\/apple-previews-ios10-biggest-ios-release-ever.html .  2016. Apple previews iOS 10 the biggest iOS release ever. http:\/\/www.apple.com\/newsroom\/2016\/06\/apple-previews-ios10-biggest-ios-release-ever.html ."},{"key":"e_1_2_2_2_1","unstructured":"2019. scikit-learn: Standardization or mean removal and variance scaling. https:\/\/scikit-learn.org\/stable\/modules\/ preprocessing.html#preprocessing-scaler  2019. scikit-learn: Standardization or mean removal and variance scaling. https:\/\/scikit-learn.org\/stable\/modules\/ preprocessing.html#preprocessing-scaler"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978318"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009890"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978371"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978391"},{"key":"e_1_2_2_8_1","volume-title":"Justin Hsu, Aaron Roth, and Pierre-Yves Strub.","author":"Barthe Gilles","year":"2015","unstructured":"Gilles Barthe , Marco Gaboardi , Emilio Jes\u00fas Gallego Arias , Justin Hsu, Aaron Roth, and Pierre-Yves Strub. 2015 . HigherOrder Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. In POPL. ACM , 55\u201368. Gilles Barthe, Marco Gaboardi, Emilio Jes\u00fas Gallego Arias, Justin Hsu, Aaron Roth, and Pierre-Yves Strub. 2015. HigherOrder Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. In POPL. ACM, 55\u201368."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2893582.2893591"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2492061"},{"key":"e_1_2_2_12_1","volume-title":"International Colloquium on Automata, Languages, and Programming","author":"Barthe Gilles","unstructured":"Gilles Barthe and Federico Olmedo . 2013. Beyond differential privacy: Composition theorems and relational logic for fdivergences between probabilistic programs . In International Colloquium on Automata, Languages, and Programming . Springer , 49\u201360. Gilles Barthe and Federico Olmedo. 2013. Beyond differential privacy: Composition theorems and relational logic for fdivergences between probabilistic programs. In International Colloquium on Automata, Languages, and Programming. Springer, 49\u201360."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2014.56"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2014.56"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3188745.3188946"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53641-4_24"},{"key":"e_1_2_2_17_1","volume-title":"Journal of Machine Learning Research","author":"Chaudhuri Kamalika","year":"2011","unstructured":"Kamalika Chaudhuri , Claire Monteleoni , and Anand D Sarwate . 2011 . Differentially private empirical risk minimization . Journal of Machine Learning Research 12, Mar (2011), 1069\u20131109. Kamalika Chaudhuri, Claire Monteleoni, and Anand D Sarwate. 2011. Differentially private empirical risk minimization. Journal of Machine Learning Research 12, Mar (2011), 1069\u20131109."},{"key":"e_1_2_2_18_1","unstructured":"Kamalika Chaudhuri and Staal A Vinterbo. 2013. A stability-based validation procedure for differentially private machine learning. In Advances in Neural Information Processing Systems. 2652\u20132660.  Kamalika Chaudhuri and Staal A Vinterbo. 2013. A stability-based validation procedure for differentially private machine learning. In Advances in Neural Information Processing Systems. 2652\u20132660."},{"key":"e_1_2_2_19_1","volume-title":"Bidirectional Type Checking for Relational Properties. CoRR abs\/1812.05067","author":"\u00c7i\u00e7ek Ezgi","year":"2018","unstructured":"Ezgi \u00c7i\u00e7ek , Weihao Qu , Gilles Barthe , Marco Gaboardi , and Deepak Garg . 2018. Bidirectional Type Checking for Relational Properties. CoRR abs\/1812.05067 ( 2018 ). arXiv: 1812.05067 http:\/\/arxiv.org\/abs\/1812.05067 Ezgi \u00c7i\u00e7ek, Weihao Qu, Gilles Barthe, Marco Gaboardi, and Deepak Garg. 2018. Bidirectional Type Checking for Relational Properties. CoRR abs\/1812.05067 (2018). arXiv: 1812.05067 http:\/\/arxiv.org\/abs\/1812.05067"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2746325.2746335"},{"key":"e_1_2_2_21_1","volume-title":"Metric Semantics for Probabilistic Relational Reasoning. CoRR abs\/1807.05091","author":"de Amorim Arthur Azevedo","year":"2018","unstructured":"Arthur Azevedo de Amorim , Marco Gaboardi , Justin Hsu , and Shin-ya Katsumata. 2018. Metric Semantics for Probabilistic Relational Reasoning. CoRR abs\/1807.05091 ( 2018 ). arXiv: 1807.05091 http:\/\/arxiv.org\/abs\/1807.05091 Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, and Shin-ya Katsumata. 2018. Metric Semantics for Probabilistic Relational Reasoning. CoRR abs\/1807.05091 (2018). arXiv: 1807.05091 http:\/\/arxiv.org\/abs\/1807.05091"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11787006_1"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1536414.1536466"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11681878_14"},{"key":"e_1_2_2_25_1","doi-asserted-by":"crossref","unstructured":"Cynthia Dwork Aaron Roth etal 2014. The algorithmic foundations of differential privacy. Foundations and Trends\u00ae in Theoretical Computer Science 9 3\u20134 (2014) 211\u2013407.  Cynthia Dwork Aaron Roth et al. 2014. The algorithmic foundations of differential privacy. Foundations and Trends\u00ae in Theoretical Computer Science 9 3\u20134 (2014) 211\u2013407.","DOI":"10.1561\/0400000042"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813677"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11257-016-9177-7"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3035940"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3187009.3177733"},{"key":"e_1_2_2_32_1","volume-title":"Towards Practical Differential Privacy for SQL Queries. CoRR abs\/1706.09479","author":"Johnson Noah M.","year":"2017","unstructured":"Noah M. Johnson , Joseph P. Near , and Dawn Xiaodong Song . 2017. Towards Practical Differential Privacy for SQL Queries. CoRR abs\/1706.09479 ( 2017 ). http:\/\/arxiv.org\/abs\/1706.09479 Noah M. Johnson, Joseph P. Near, and Dawn Xiaodong Song. 2017. Towards Practical Differential Privacy for SQL Queries. CoRR abs\/1706.09479 (2017). http:\/\/arxiv.org\/abs\/1706.09479"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE.2008.4497436"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2007.66"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1559845.1559850"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1559845.1559850"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.11"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2213836.2213876"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_2_2_40_1","volume-title":"Presented as part of the 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI 12). 149\u2013162.","author":"Narayan Arjun","unstructured":"Arjun Narayan and Andreas Haeberlen . 2012. DJoin: differentially private join queries over distributed databases . In Presented as part of the 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI 12). 149\u2013162. Arjun Narayan and Andreas Haeberlen. 2012. DJoin: differentially private join queries over distributed databases. In Presented as part of the 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI 12). 149\u2013162."},{"key":"e_1_2_2_41_1","volume-title":"Duet: An Expressive Higher-order Language and Linear Type System for Statically Enforcing Differential Privacy. CoRR abs\/1909.02481","author":"Near Joseph P.","year":"2019","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. CoRR abs\/1909.02481 (2019). https:\/\/arxiv.org\/abs\/1909.02481 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. CoRR abs\/1909.02481 (2019). https:\/\/arxiv.org\/abs\/1909.02481"},{"key":"e_1_2_2_42_1","volume-title":"Semi-supervised knowledge transfer for deep learning from private training data. arXiv preprint arXiv:1610.05755","author":"Papernot Nicolas","year":"2016","unstructured":"Nicolas Papernot , Mart\u00edn Abadi , Ulfar Erlingsson , Ian Goodfellow , and Kunal Talwar . 2016. Semi-supervised knowledge transfer for deep learning from private training data. arXiv preprint arXiv:1610.05755 ( 2016 ). Nicolas Papernot, Mart\u00edn Abadi, Ulfar Erlingsson, Ian Goodfellow, and Kunal Talwar. 2016. Semi-supervised knowledge transfer for deep learning from private training data. arXiv preprint arXiv:1610.05755 (2016)."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.14778\/2732296.2732300"},{"key":"e_1_2_2_44_1","first-page":"157","article-title":"Distance makes the types grow stronger: a calculus for differential privacy","volume":"45","author":"Reed Jason","year":"2010","unstructured":"Jason Reed and Benjamin C Pierce . 2010 . Distance makes the types grow stronger: a calculus for differential privacy . ICFP 45 , 9 (2010), 157 \u2013 168 . Jason Reed and Benjamin C Pierce. 2010. Distance makes the types grow stronger: a calculus for differential privacy. ICFP 45, 9 (2010), 157\u2013168.","journal-title":"ICFP"},{"key":"e_1_2_2_45_1","first-page":"297","article-title":"Airavat: Security and Privacy for MapReduce","volume":"10","author":"Roy Indrajit","year":"2010","unstructured":"Indrajit Roy , Srinath TV Setty , Ann Kilzer , Vitaly Shmatikov , and Emmett Witchel . 2010 . Airavat: Security and Privacy for MapReduce .. In NSDI , Vol. 10. 297 \u2013 312 . Indrajit Roy, Srinath TV Setty, Ann Kilzer, Vitaly Shmatikov, and Emmett Witchel. 2010. Airavat: Security and Privacy for MapReduce.. In NSDI, Vol. 10. 297\u2013312.","journal-title":"NSDI"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2016.09.043"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785668"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.41"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/GlobalSIP.2013.6736861"},{"key":"e_1_2_2_50_1","volume-title":"Abhradeep Guha Thakurta, and Li Zhang","author":"Talwar Kunal","year":"2015","unstructured":"Kunal Talwar , Abhradeep Guha Thakurta, and Li Zhang . 2015 . Nearly optimal private lasso. In Advances in Neural Information Processing Systems . 3025\u20133033. Kunal Talwar, Abhradeep Guha Thakurta, and Li Zhang. 2015. Nearly optimal private lasso. In Advances in Neural Information Processing Systems. 3025\u20133033."},{"key":"e_1_2_2_51_1","volume-title":"Subsampled R\u00e9nyi Differential Privacy and Analytical Moments Accountant. CoRR abs\/1808.00087","author":"Wang Yu-Xiang","year":"2018","unstructured":"Yu-Xiang Wang , Borja Balle , and Shiva Kasiviswanathan . 2018. Subsampled R\u00e9nyi Differential Privacy and Analytical Moments Accountant. CoRR abs\/1808.00087 ( 2018 ). arXiv: 1808.00087 http:\/\/arxiv.org\/abs\/1808.00087 Yu-Xiang Wang, Borja Balle, and Shiva Kasiviswanathan. 2018. Subsampled R\u00e9nyi Differential Privacy and Analytical Moments Accountant. CoRR abs\/1808.00087 (2018). arXiv: 1808.00087 http:\/\/arxiv.org\/abs\/1808.00087"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.32"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3064047"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009884"},{"key":"e_1_2_2_55_1","volume-title":"Fuzzi: A Three-Level Logic for Differential Privacy. Accepted for publication in PACMPL \/ ICFP","author":"Zhang Hengchu","year":"2019","unstructured":"Hengchu Zhang , Edo Roth , Andreas Haeberlen , Benjamin C. Pierce , and Aaron Roth . 2019 . Fuzzi: A Three-Level Logic for Differential Privacy. Accepted for publication in PACMPL \/ ICFP 2019. Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. Pierce, and Aaron Roth. 2019. Fuzzi: A Three-Level Logic for Differential Privacy. Accepted for publication in PACMPL \/ ICFP 2019."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360598","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360598","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360598","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360598"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":54,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360598"],"URL":"https:\/\/doi.org\/10.1145\/3360598","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}