Formalization of Differential Privacy in Isabelle/HOL

Explore a 30-minute conference talk from CPP 2025 where researchers Tetsuya Sato and Yasuhiko Minamide from the Institute of Science Tokyo present their groundbreaking work on formalizing differential privacy using the Isabelle/HOL proof assistant. Learn about the first formalization of differential privacy that supports continuous probability distributions, addressing the challenges of verifying privacy in database programs where small changes can compromise security. The presentation covers the standard definition of differential privacy and its properties, the Laplace mechanism and its differential privacy, and the differential privacy of the report noisy max mechanism. This talk, sponsored by ACM SIGPLAN and ACM SIGLOG, offers valuable insights for researchers and practitioners interested in formal verification, program security, and privacy-preserving computation techniques.