Contextual Linear Types for Differential Privacy

TL;DR

Jazz is a new language and type system that combines linear types and latent contextual effects to support advanced differential privacy variants and higher-order programming, improving precision and modularity.

Contribution

It introduces Jazz, a language with a novel type system that supports complex differential privacy variants alongside higher-order functions, addressing previous limitations.

Findings

Formalized core of Jazz with soundness proof for privacy

Demonstrated expressive power through case studies

Enhanced analysis precision and modularity

Abstract

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 $\epsilon$-differential privacy in its original design, significant progress has been made to support more advancedvariants of differential privacy, like($\epsilon$,$\delta$)-differential privacy. However, supporting these advanced privacy variants while also supporting higher-order programming in full has proven to be challenging. 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. Latent contextual effects allow delaying the payment of effects for connectives such as products, sums and functions, yielding advantages in terms of precision of the analysis and annotation burden upon elimination, as well as modularity. We formalize the core of Jazz, 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.