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.

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.

Differential privacy enables general statistical analysis of data with formal guarantees of privacy protection at the individual level. Tools that assist data analysts with utilizing differential privacy have frequently taken the form of programming languages and libraries. However, many existing programming languages designed for compositional verification of differential privacy impose significant burden on the programmer (in the form of complex type annotations). Supplementary library support for privacy analysis built on top of existing general-purpose languages has been more usable, but incapable of pervasive end-to-end enforcement of sensitivity analysis and privacy composition. We introduce DDuo, a dynamic analysis for enforcing differential privacy. DDuo is usable by non-experts: its analysis is automatic and it requires no additional type annotations. DDuo can be implemented as a library for existing programming languages; we present a reference implementation in Python which features moderate runtime overheads on realistic workloads. We include support for several data types, distance metrics and operations which are commonly used in modern machine learning programs. We also provide initial support for tracking the sensitivity of data transformations in popular Python libraries for data analysis. We formalize the novel core of the DDuo system and prove it sound for sensitivity analysis via a logical relation for metric preservation. We also illustrate DDuo's usability and flexibility through various case studies which implement state-of-the-art machine learning algorithms.

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. We propose Duet, an expressive higher-order language, linear type system and tool for automatically verifying differential privacy of general-purpose higher-order programs. In addition to general purpose programming, Duet supports encoding machine learning algorithms such as stochastic gradient descent, as well as common auxiliary data analysis tasks such as clipping, normalization and hyperparameter tuning - each of which are particularly challenging to encode in a statically verified differential privacy framework. We present a core design of the Duet language and linear type system, and complete key proofs about privacy for well-typed programs. We then show how to extend Duet to support realistic machine learning applications and recent variants of differential privacy which result in improved accuracy for many practical differentially private algorithms. Finally, we implement several differentially private machine learning algorithms in Duet which have never before been automatically verified by a language-based tool, and we present experimental results which demonstrate the benefits of Duet's language design in terms of accuracy of trained machine learning models.

Assessing students' learning of concepts in programming is an essential part of teaching computer science. We developed the Tablet Game, an embedded assessment that measures students' skill in identifying programming structures used to create various behaviors in MIT App Inventor. The assessment was implemented as an app for Android devices. Students conducted an activity in the app, and identified which code-blocks would create those behaviors. Students' responses were transmitted to our custom data-collection server. In two five-day app development summer camps held with middle school students, students completed the same Tablet Game assessment on day 1 and day 5. Students also completed pre/post surveys which gathered ethnographic data and asked about interest levels in computer science and prior programming experience. Using data from 44 students with pre/post assessments matched to surveys, our results indicated that (1) students with high self-reported prior experience in App Inventor outperformed students with low prior experience on the Tablet Game pre-test, indicating that the assessment measures programming skill and (2) students with low prior experience achieved equivalent results as the high prior experience cohort in the post-test, indicating that the camp was successful in imparting programming skills. Both of these results are statistically significant. Further, (3) there were no statistically significant differences in gender composition of the two experience cohorts, indicating that the camp was equally accessible to girls and boys.