48 citations · 51 across the 3 of their papers we have counts for
6 papers · 1 filter
Solo: A Lightweight Static Analysis for Differential Privacy
Chike Abuah, David Darais, Joseph P. Near
All current approaches for statically enforcing differential privacy in higher order languages make use of either linear or relational refinement types. A barrier to adoption for t…
DDUO: General-Purpose Dynamic Analysis for Differential Privacy
Chike Abuah, Alex Silence, David Darais +1
Differential privacy enables general statistical analysis of data with formal guarantees of privacy protection at the individual level. Tools that assist data analysts with utilizi…
Duet: An Expressive Higher-order Language and Linear Type System for Statically Enforcing Differential Privacy
Joseph P. Near, David Darais, Chike Abuah +8
During the past decade, differential privacy has become the gold standard for protecting the privacy of individuals. However, verifying that a particular program provides different…
Constructive Galois Connections
David Darais, David Van Horn
Galois connections are a foundational tool for structuring abstraction in semantics and their use lies at the heart of the theory of abstract interpretation. Yet, mechanization of…
Abstracting Definitional Interpreters
David Darais, Nicholas Labich, Phuc C. Nguyen +1
In this functional pearl, we examine the use of definitional interpreters as a basis for abstract interpretation of higher-order programming languages. As it turns out, definitiona…
Mechanically Verified Calculational Abstract Interpretation
David Darais, David Van Horn
Calculational abstract interpretation, long advocated by Cousot, is a technique for deriving correct-by-construction abstract interpreters from the formal semantics of programming…