Duet: an expressive higher-order language and linear type system for statically enforcing differential privacy
Abstract
During the past decade, differential privacy has become the gold standard for protecting the privacy of individuals. However, verifying that a particular program provides differential privacy often remains a manual task to be completed by an expert in the field. Language-based techniques have been proposed for fully automating proofs of differential privacy via type system design, however these results have lagged behind advances in differentially-private algorithms, leaving a noticeable gap in programs which can be automatically verified while also providing state-of-the-art bounds on privacy.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Oct 10, 2019
- Source ID
- 10.1145/3360598
Entities
People
- Alex Shan
- Chike Abuah
- David Darais
- Dawn Song
- Joseph P. Near
- Lun Wang
- Mu Zhang
- Neel Somani
- Nikhil Sharma
- Pranav Gaddamadugu
- Tim Stevens
Organizations
- Defense Advanced Research Projects Agency
- Intelligence Advanced Research Projects Activity
- National Science Foundation
- University of California, Berkeley
- University of Utah
- University of Vermont