一句话：提出 Solo 类型系统，无需线性或关系细化类型即可静态强制差分隐私，并可嵌入 Haskell。
现有在高阶语言中静态强制差分隐私的方法依赖线性类型或关系细化类型，但主流语言缺乏对这些“花式类型”的支持：没有主流语言支持关系细化类型，Rust 和现代 Haskell 的线性类型技术也不足以嵌入差分隐私所需的“完全”线性类型。本文提出 Solo 类型系统，不再使用线性类型和关系细化类型，而是可轻松嵌入 Haskell 等具有丰富类型系统的语言。作者在 Haskell 中实现了该嵌入，通过案例研究展示其表达力，并证明了基于类型的差分隐私强制具有可靠性。
Existing approaches for statically enforcing differential privacy in higher order languages use either linear or relational refinement types. A barrier to adoption for these approaches is the lack of support for expressing these “fancy types” in mainstream programming languages. For example, no mainstream language supports relational refinement types, and although Rust and modern versions of Haskell both employ some linear typing techniques, they are inadequate for embedding enforcement of differential privacy, which requires “full” linear types. We propose a new type system that enforces differential privacy, avoids the use of linear and relational refinement types, and can be easily embedded in richly typed programming languages like Haskell. We demonstrate such an embedding in Haskell, demonstrate its expressiveness on case studies, and prove soundness of our type-based enforcement of differential privacy.
@article{paperbot1452,
title = {Solo: a lightweight static analysis for differential privacy},
author = {Chiké Abuah and David Darais and Joseph P. Near},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563313}
}