Contextual Linear Types for Differential Privacy
share
Language support for differentially-private programming is both crucial and delicate. While elaborate program logics can be very expressive, type-system based approaches using linear types tend to be more lightweight and amenable to automatic checking and inference, and in particular in the presence of higher-order programming. Since the seminal design of Fuzz, which is restricted to ϵ-differential privacy, a lot of effort has been made to support more advanced variants of differential privacy, like (ϵ,δ)-differential privacy. However, no existing type system supports these advanced privacy variants while also supporting higher-order programming in full generality. We present Jazz, a language and type system which uses linear types and latent contextual effects to support both advanced variants of differential privacy and higher order programming . Even when avoiding advanced variants and higher order programming, our system achieves higher precision than prior work for a large class of programming patterns. We formalize the core of the Jazz language, prove it sound for privacy via a logical relation for metric preservation, and illustrate its expressive power through a number of case studies drawn from the recent differential privacy literature.
READ FULL TEXT