Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Differential Privacy (using Qua...

Email Gateway (Feb 02 2025 at 21:26):

From: Tobias Nipkow <nipkow@in.tum.de>
Differential Privacy
Tetsuya Sato and Yasuhiko Minamide

This entry contains formalization of differential privacy in a general setting,
based on the seminal textbook of Dwork and Roth and the papers of statistical
divergence for differential privacy [Sato and Katsumata, MSCS2023 and Barthe and
Olmedo,ICALP2013].

This entry includes the following formalization:

• Measurable space of lists and measurability of list operations
• Laplace distribution
• The statisatical divergence for differential privacy
• Differential privacy and its basic properties
• Randomized Response
• Laplace mechanismhttps://www.isa-afp.org/entries/DP_QBS.html
• The report noisy max mechanism

https://www.isa-afp.org/entries/Differential_Privacy.html

Differential Privacy using Quasi-Borel Spaces
Michikazu Hirata

This entry formalizes differential privacy using quasi-Borel spaces. In general,
differential privacy is discussed using measurable spaces. Sato and Katsumata
showed that quasi-Borel spaces are also applied to formulate differential
privacy. We formalize basic definitions and properties of differential privacy
using quasi-Borel spaces, and show two examples: randomized response and the
naive report noisy max algorithm.

https://www.isa-afp.org/entries/DP_QBS.html

Enjoy & Enjoy!

smime.p7s

Last updated: Mar 09 2025 at 12:28 UTC