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.

翻译：语言支持差分隐私编程既至关重要又十分精密。尽管精细的程序逻辑可以具有很高的表达能力，但使用线性类型的基于类型系统的方法往往更轻量级，并且更适合自动检查和推理，尤其是在存在高阶编程的情况下。自最初设计受限为$\epsilon$-差分隐私的开创性Fuzz设计以来，为了支持更高级的差分隐私变体（如($\epsilon$,$\delta$)-差分隐私），已经取得了显著进展。然而，在完整支持高阶编程的同时支持这些高级隐私变体已被证明具有挑战性。我们提出Jazz，一种使用线性类型和潜在上下文效应来支持高级差分隐私变体及高阶编程的语言和类型系统。潜在上下文效应允许延迟对连接词（如乘积、和与函数）支付效应，从而在分析的精确性、消除时的标注负担以及模块化方面带来优势。我们形式化了Jazz的核心，通过度量保持的逻辑关系证明了其隐私安全性，并通过来自近期差分隐私文献的若干案例研究展示了其表达能力。