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
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 View reference page