{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,5]],"date-time":"2026-03-05T16:19:52Z","timestamp":1772727592736,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":60,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T00:00:00Z","timestamp":1736467200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Japan Society for the Promotion of Science","award":["JP20H04162, JP24K14891, JP20K19775, JP24K14893"],"award-info":[{"award-number":["JP20H04162, JP24K14891, JP20K19775, JP24K14893"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,1,10]]},"DOI":"10.1145\/3703595.3705875","type":"proceedings-article","created":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T21:23:16Z","timestamp":1736544196000},"page":"67-82","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Formalization of Differential Privacy in Isabelle\/HOL"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9895-9209","authenticated-orcid":false,"given":"Tetsuya","family":"Sato","sequence":"first","affiliation":[{"name":"Institute of Science Tokyo, Meguro, Japan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8647-6816","authenticated-orcid":false,"given":"Yasuhiko","family":"Minamide","sequence":"additional","affiliation":[{"name":"Institute of Science Tokyo, Meguro, Japan"}]}],"member":"320","published-online":{"date-parts":[[2025,1,10]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575691"},{"key":"e_1_3_2_2_2_1","volume-title":"Towards the Fundamental Theorem of Calculus for the Lebesgue Integral in Coq. In 35es Journ\u00e9es Francophones des Langages Applicatifs (JFLA","author":"Affeldt Reynald","year":"2024","unstructured":"Reynald Affeldt and Zachary Stone. 2024. Towards the Fundamental Theorem of Calculus for the Lebesgue Integral in Coq. In 35es Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2024). Saint-Jacut-de-la-Mer, France. https:\/\/inria.hal.science\/hal-04406350"},{"key":"e_1_3_2_2_3_1","volume-title":"Differential Privacy Overview. https:\/\/www.apple.com\/privacy\/docs\/Differential_Privacy_Overview.pdf Accessed","author":"Apple Inc.","year":"2024","unstructured":"Apple Inc.. 2017. Differential Privacy Overview. https:\/\/www.apple.com\/privacy\/docs\/Differential_Privacy_Overview.pdf Accessed: September 12, 2024"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAIT.2021.3054692"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1215\/ijm"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9404-x"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v33i01.33012662"},{"key":"e_1_3_2_2_8_1","volume-title":"Proceedings of the Twenty Third International Conference on Artificial Intelligence and Statistics (AISTATS","volume":"2506","author":"Balle Borja","year":"2020","unstructured":"Borja Balle, Gilles Barthe, Marco Gaboardi, Justin Hsu, and Tetsuya Sato. 2020. Hypothesis Testing Interpretations and Renyi Differential Privacy. In Proceedings of the Twenty Third International Conference on Artificial Intelligence and Statistics (AISTATS 2020), Silvia Chiappa and Roberto Calandra (Eds.) (Proceedings of Machine Learning Research, Vol. 108). PMLR, Online. 2496\u20132506. http:\/\/proceedings.mlr.press\/v108\/balle20a.html"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978391"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677000"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103670"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_8"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-019-09341-z"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"crossref","unstructured":"Nick Benton. 2004. Simple Relational Correctness Proofs for Static Analyses and Program Transformations. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201904) (proceedings of the 31st acm sigplan-sigact symposium on principles of programming languages (popl \u201904) ed.). ACM 43. https:\/\/www.microsoft.com\/en-us\/research\/publication\/simple-relational-correctness-proofs-for-static-analyses-and-program-transformations\/","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-021-09612-0"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_4"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53641-4_24"},{"key":"e_1_3_2_2_19_1","unstructured":"Cl\u00e9ment L. Canonne Gautam Kamath and Thomas Steinke. 2021. The Discrete Gaussian for Differential Privacy. arxiv:2004.00010. arxiv:2004.00010"},{"key":"e_1_3_2_2_20_1","first-page":"299","article-title":"Information-type measures of difference of probability distributions and indirect observations. Studia Sci","volume":"2","author":"Csisz\u00e1r I.","year":"1967","unstructured":"I. Csisz\u00e1r. 1967. Information-type measures of difference of probability distributions and indirect observations. Studia Sci. Math. Hungar., 2 (1967), 299\u2013318.","journal-title":"Math. Hungar."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2746325.2746335"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1111\/rssb.12454"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11787006_1"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11761679_29"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11681878_14"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1561\/0400000042"},{"key":"e_1_3_2_2_27_1","unstructured":"Manuel Eberl. 2018. The Error Function. Archive of Formal Proofs February issn:2150-914x https:\/\/isa-afp.org\/entries\/Error_Function.html"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_4"},{"key":"e_1_3_2_2_29_1","volume-title":"ACM Symposium on Principles of Programming Languages (POPL\u201913)","author":"Gaboardi Marco","unstructured":"Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. 2013. Linear dependent types for differential privacy. In ACM Symposium on Principles of Programming Languages (POPL\u201913). 357\u2013370. http:\/\/dl.acm.org\/citation.cfm?id=2429113"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0092872"},{"key":"e_1_3_2_2_31_1","volume-title":"Enabling developers and organizations to use differential privacy. 5 September, https:\/\/developers.googleblog.com\/en\/enabling-developers-and-organizations-to-use-differential-privacy\/ Accessed","author":"Guevara Miguel","year":"2024","unstructured":"Miguel Guevara. 2019. Enabling developers and organizations to use differential privacy. 5 September, https:\/\/developers.googleblog.com\/en\/enabling-developers-and-organizations-to-use-differential-privacy\/ Accessed: September 12, 2024"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005137"},{"key":"e_1_3_2_2_33_1","unstructured":"Michikazu Hirata. 2024. Coproduct Measure. Archive of Formal Proofs June issn:2150-914x https:\/\/isa-afp.org\/entries\/Coproduct_Measure.html"},{"key":"e_1_3_2_2_34_1","volume-title":"Program Logic for Higher-Order Probabilistic Programs in Isabelle\/HOL","author":"Hirata Michikazu","unstructured":"Michikazu Hirata, Yasuhiko Minamide, and Tetsuya Sato. 2022. Program Logic for Higher-Order Probabilistic Programs in Isabelle\/HOL. In Functional and Logic Programming, Michael Hanus and Atsushi Igarashi (Eds.). Springer International Publishing, Cham. 57\u201374. isbn:978-3-030-99461-7"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2023.18"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018628"},{"key":"e_1_3_2_2_37_1","volume-title":"Three","author":"H\u00f6lzl Johannes","year":"2011","unstructured":"Johannes H\u00f6lzl, Armin Heller, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk. 2011. Three Chapters of Measure Theory in Isabelle\/HOL. In Interactive Theorem Proving (ITP 2011). Springer Berlin Heidelberg, 135\u2013151. isbn:978-3-642-22863-6"},{"key":"e_1_3_2_2_38_1","unstructured":"Fabian Immler. 2019. Laplace Transform. Archive of Formal Proofs August issn:2150-914x https:\/\/isa-afp.org\/entries\/Laplace_Transform.html"},{"key":"e_1_3_2_2_39_1","volume-title":"25th Workshop on Programming and Programming Languages (PPL2023)","author":"Ishiguro Yoshihiro","year":"2023","unstructured":"Yoshihiro Ishiguro and Reynald Affeldt. 2023. A Progress Report on Formalization of Measure Theory with MathComp-Analysis. In 25th Workshop on Programming and Programming Languages (PPL2023), Nagoya University, March 6\u20138, 2023. https:\/\/staff.aist.go.jp\/reynald.affeldt\/documents\/measure-ppl2023.pdf Conference website:"},{"key":"e_1_3_2_2_40_1","volume-title":"Proceedings of the 32nd International Conference on Machine Learning, ICML 2015","author":"Kairouz Peter","year":"2015","unstructured":"Peter Kairouz, Sewoong Oh, and Pramod Viswanath. 2015. The Composition Theorem for Differential Privacy. In Proceedings of the 32nd International Conference on Machine Learning, ICML 2015, Lille, France, 6-11 July 2015. 1376\u20131385. http:\/\/jmlr.org\/proceedings\/papers\/v37\/kairouz15.html"},{"key":"e_1_3_2_2_41_1","unstructured":"Emin Karayel and Manuel Eberl. 2023. Executable Randomized Algorithms. Archive of Formal Proofs June issn:2150-914x https:\/\/isa-afp.org\/entries\/Executable_Randomized_Algorithms.html"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01220868"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.2006.881731"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_20"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.14778\/3055330.3055331"},{"key":"e_1_3_2_2_46_1","volume-title":"API Documentation of Lean 4. https:\/\/leanprover-community.github.io\/mathlib4_docs\/ Accessed","author":"Community The","year":"2024","unstructured":"The mathlib Community. 2024. API Documentation of Lean 4. https:\/\/leanprover-community.github.io\/mathlib4_docs\/ Accessed: September 12, 2024"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382264"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.11"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2741948.2741978"},{"key":"e_1_3_2_2_50_1","volume-title":"Paulson","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. 2002. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag, Berlin, Heidelberg. isbn:3540433767"},{"key":"e_1_3_2_2_51_1","volume-title":"Approximate Relational Reasoning for Probabilistic Programs. Ph. D. Dissertation","author":"Olmedo Federico","unstructured":"Federico Olmedo. 2014. Approximate Relational Reasoning for Probabilistic Programs. Ph. D. Dissertation. Technical University of Madrid."},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2016.09.043"},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785668"},{"key":"e_1_3_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129523000245"},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158148"},{"key":"e_1_3_2_2_56_1","volume-title":"Commutative Semantics for Probabilistic Programming","author":"Staton Sam","unstructured":"Sam Staton. 2017. Commutative Semantics for Probabilistic Programming. In Programming Languages and Systems, Hongseok Yang (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 855\u2013879. isbn:978-3-662-54434-1"},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3589207"},{"key":"e_1_3_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.11204806"},{"key":"e_1_3_2_2_59_1","unstructured":"Jean-Baptiste Tristan Joseph Tassarotti Koundinya Vajjha Michael L. Wick and Anindya Banerjee. 2020. Verification of ML Systems via Reparameterization. arxiv:2007.06776."},{"key":"e_1_3_2_2_60_1","unstructured":"Lei Yu. 2013. A Formal Model of IEEE Floating Point Arithmetic. Archive of Formal Proofs July issn:2150-914x https:\/\/isa-afp.org\/entries\/IEEE_Floating_Point.html"}],"event":{"name":"CPP '25: 14th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Denver CO USA","acronym":"CPP '25","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG"]},"container-title":["Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705875","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3703595.3705875","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:08Z","timestamp":1750295888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705875"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,10]]},"references-count":60,"alternative-id":["10.1145\/3703595.3705875","10.1145\/3703595"],"URL":"https:\/\/doi.org\/10.1145\/3703595.3705875","relation":{},"subject":[],"published":{"date-parts":[[2025,1,10]]},"assertion":[{"value":"2025-01-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}