一句话：提出 Jazz：用线性类型与潜在上下文效应支持高阶程序及高级差分隐私变体的语言与类型系统。
差分隐私编程的语言支持既关键又微妙。程序逻辑表达力强但较重，基于线性类型的方法更轻量、便于自动检查与推断，尤其适合高阶编程；但兼顾 (ε,δ)-差分隐私等高级变体与完整高阶编程仍很困难。本文提出 Jazz：一种用线性类型和潜在上下文效应（latent contextual effects）的语言与类型系统，通过延迟积、和、函数等连接词的效应支付，兼顾高级差分隐私与高阶编程，并提升分析精度、减少标注负担与增强模块化。作者形式化核心，用度量保持的逻辑关系证明隐私可靠性，并以近期文献案例展示表达力。
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 in its original design, significant progress has been made to support more advanced variants of differential privacy, like (ϵ, δ )-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.
@article{paperbot2133,
title = {Contextual Linear Types for Differential Privacy},
author = {Matías Toro and David Darais and Chike Abuah and Joseph P. Near and Damián Árquez and Federico Olmedo and Éric Tanter},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {45},
number = {2},
year = {2023},
doi = {10.1145/3589207}
}