Existing approaches for statically enforcing differential privacy in higher order languages use either linear or relational refinement types. A barrier to adoption for these approaches is the lack of support for expressing these “fancy types” in mainstream programming languages. For example, no mainstream language supports relational refinement types, and although Rust and modern versions of Haskell both employ some linear typing techniques, they are inadequate for embedding enforcement of differential privacy, which requires “full” linear types. We propose a new type system that enforces differential privacy, avoids the use of linear and relational refinement types, and can be easily embedded in richly typed programming languages like Haskell. We demonstrate such an embedding in Haskell, demonstrate its expressiveness on case studies, and prove soundness of our type-based enforcement of differential privacy.
Thu 8 DecDisplayed time zone: Auckland, Wellington change
10:30 - 12:00 | |||
10:30 30mResearch paper | C to checked C by 3c OOPSLA Aravind Machiry Purdue University, John Kastner Amazon, Matt McCutchen , Aaron Eline Amazon, Kyle Headley Amazon, MIchael Hicks Amazon DOI | ||
11:00 30mTalk | Solo: A Lightweight Static Analysis for Differential Privacy OOPSLA DOI | ||
11:30 30mTalk | MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types OOPSLA Lionel Parreaux Hong Kong University of Science and Technology, Chun Yin Chau The Hong Kong University of Science and Technology DOI Pre-print Media Attached File Attached |