{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:41Z","timestamp":1780994561977,"version":"3.54.1"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"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":["CNS-1065060,CNS-1513694"],"award-info":[{"award-number":["CNS-1065060,CNS-1513694"]}],"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":[[2019,7,26]]},"abstract":"<jats:p>\n            Curators of sensitive datasets sometimes need to know whether queries against the data are\n            <jats:italic>differentially private<\/jats:italic>\n            . Two sorts of logics have been proposed for checking this property: (1)\n            <jats:italic>type systems<\/jats:italic>\n            and other static analyses, which fully automate straightforward reasoning with concepts like \u201cprogram sensitivity\u201d and \u201cprivacy loss,\u201d and (2) full-blown program logics such as apRHL (an approximate, probabilistic, relational Hoare logic), which support more flexible reasoning about subtle privacy-preserving algorithmic techniques but offer only minimal automation.\n          <\/jats:p>\n          <jats:p>\n            We propose a\n            <jats:italic>three-level logic<\/jats:italic>\n            for differential privacy in an imperative setting and present a prototype implementation called Fuzzi. Fuzzi\u2019s lowest level is a general-purpose logic; its middle level is apRHL; and its top level is a novel\n            <jats:italic>sensitivity logic<\/jats:italic>\n            adapted from the linear-logic-inspired type system of Fuzz, a differentially private functional language. The key novelty is a high degree of integration between the sensitivity logic and the two lower-level logics: the judgments and proofs of the sensitivity logic can be easily translated into apRHL; conversely, privacy properties of key algorithmic building blocks can be proved manually in apRHL and the base logic, then packaged up as typing rules that can be applied by a checker for the sensitivity logic to automatically construct privacy proofs for composite programs of arbitrary size.\n          <\/jats:p>\n          <jats:p>We demonstrate Fuzzi\u2019s utility by implementing four different private machine-learning algorithms and showing that Fuzzi\u2019s checker is able to derive tight sensitivity bounds.<\/jats:p>","DOI":"10.1145\/3341697","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Fuzzi: a three-level logic for differential privacy"],"prefix":"10.1145","volume":"3","author":[{"given":"Hengchu","family":"Zhang","sequence":"first","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Edo","family":"Roth","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andreas","family":"Haeberlen","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Benjamin C.","family":"Pierce","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aaron","family":"Roth","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978318"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158146"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_2_2_6_1","unstructured":"Apple. 2017. Apple Differential Privacy Whitepaper. https:\/\/images.apple.com\/privacy\/docs\/Differential_Privacy_Overview. pdf  Apple. 2017. Apple Differential Privacy Whitepaper. https:\/\/images.apple.com\/privacy\/docs\/Differential_Privacy_Overview. pdf"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2036918.2036930"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043621.2043626"},{"key":"e_1_2_2_11_1","volume-title":"On the Privacy Properties of Variants on the Sparse Vector Technique. CoRR abs\/1508.07306","author":"Chen Yan","year":"2015"},{"key":"e_1_2_2_12_1","unstructured":"The Coq Development Team. 2018. The Coq Proof Assistant Reference Manual version 8.8. http:\/\/coq.inria.fr  The Coq Development Team. 2018. The Coq Proof Assistant Reference Manual version 8.8. http:\/\/coq.inria.fr"},{"key":"e_1_2_2_13_1","unstructured":"Dua Dheeru and Efi Karra Taniskidou. 2017. UCI Machine Learning Repository. http:\/\/archive.ics.uci.edu\/ml  Dua Dheeru and Efi Karra Taniskidou. 2017. UCI Machine Learning Repository. http:\/\/archive.ics.uci.edu\/ml"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243818"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11681878_14"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1561\/0400000042"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2010.12"},{"key":"e_1_2_2_18_1","unstructured":"The EasyCrypt Development Team. 2018. EasyCrypt Reference Manual version 1.x. https:\/\/www.easycrypt.info\/ documentation\/refman.pdf  The EasyCrypt Development Team. 2018. EasyCrypt Reference Manual version 1.x. https:\/\/www.easycrypt.info\/ documentation\/refman.pdf"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1469-1809.1936.tb02137.x"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_2_2_22_1","volume-title":"Vadhan","author":"Gaboardi Marco","year":"2016"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/2028067.2028100"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_25_1","unstructured":"Justin Hsu. 2018. Private Communication.  Justin Hsu. 2018. Private Communication."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3187009.3177733"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.726791"},{"key":"e_1_2_2_29_1","unstructured":"Yann LeCun and Corinna Cortes. 2010. MNIST handwritten digit database. http:\/\/yann.lecun.com\/exdb\/mnist\/. (2010). http:\/\/yann.lecun.com\/exdb\/mnist\/  Yann LeCun and Corinna Cortes. 2010. MNIST handwritten digit database. http:\/\/yann.lecun.com\/exdb\/mnist\/. (2010). http:\/\/yann.lecun.com\/exdb\/mnist\/"},{"key":"e_1_2_2_30_1","volume-title":"Understanding the Sparse Vector Technique for Differential Privacy. CoRR abs\/1603.01699","author":"Lyu Min","year":"2016"},{"key":"e_1_2_2_31_1","volume-title":"Learning Differentially Private Recurrent Language Models. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=BJ0hF1Z0b","author":"McMahan H. Brendan","year":"2018"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1557019.1557090"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1559845.1559850"},{"key":"e_1_2_2_34_1","unstructured":"Microsoft. 2017. Collecting telemetry data privately. https:\/\/www.microsoft.com\/en-us\/research\/blog\/collecting-telemetrydata-privately\/  Microsoft. 2017. Collecting telemetry data privately. https:\/\/www.microsoft.com\/en-us\/research\/blog\/collecting-telemetrydata-privately\/"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382264"},{"key":"e_1_2_2_36_1","volume-title":"Abowd","author":"Dajani Aref N.","year":"2017"},{"key":"e_1_2_2_37_1","volume-title":"Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201912)","author":"Narayan Arjun","year":"2012"},{"key":"e_1_2_2_38_1","unstructured":"Joseph P. Near David Darais Tim Stevens Paranav Gaddamadugu Lun Wang Neel Somani Mu Zhang Nikhil Sharma Alex Shan and Dawn Song. 2019. (2019). http:\/\/david.darais.com\/assets\/papers\/duet\/duet.pdf  Joseph P. Near David Darais Tim Stevens Paranav Gaddamadugu Lun Wang Neel Somani Mu Zhang Nikhil Sharma Alex Shan and Dawn Song. 2019. (2019). http:\/\/david.darais.com\/assets\/papers\/duet\/duet.pdf"},{"key":"e_1_2_2_39_1","volume-title":"Guide to NumPy","author":"Oliphant Travis E.","edition":"2"},{"key":"e_1_2_2_40_1","volume-title":"Semi-supervised Knowledge Transfer for Deep Learning from Private Training Data. arXiv:1610.05755 {cs, stat} (Oct","author":"Papernot Nicolas","year":"2016"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1932681.1863568"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_2_43_1","volume-title":"Advances in Neural Information Processing Systems 29","author":"Rogers Ryan M","year":"1921"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2016.09.043"},{"key":"e_1_2_2_45_1","volume-title":"Approximate Span Liftings. CoRR abs\/1710.09010","author":"Sato Tetsuya","year":"2019"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110254"},{"key":"e_1_2_2_48_1","first-page":"1","article-title":"LightDP","volume":"52","author":"Zhang Danfeng","year":"2017","journal-title":"Towards Automating Differential Privacy Proofs. SIGPLAN Not."},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183713.3196921"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341697","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341697","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341697","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:30Z","timestamp":1750200090000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341697"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":49,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341697"],"URL":"https:\/\/doi.org\/10.1145\/3341697","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}