View publication
| Title | Contextual Linear Types for Differential Privacy |
| Authors | Matías Toro, David Darais, Chike Abuah, Joseph Near, Damián Árquez, Federico Olmedo, Éric Tanter |
| Publication date | 2023 |
| 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 advanced variants 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 that 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. |
| Pages | 8:1-8:69 |
| Volume | 45 |
| Journal name | ACM Transactions on Programming Languages and Systems |
| Publisher | ACM Press (New York, NY, USA) |
| Reference URL |
|