research
∙
07/18/2023
Stream Types
We propose a rich foundational theory of typed data streams and stream t...
share
research
∙
03/01/2022
Parsing Randomness: Unifying and Differentiating Parsers and Random Generators
"A generator is a parser of randomness." This perspective on generators ...
research
∙
05/02/2021
Security Properties for Stack Safety
What exactly does "stack safety" mean? The phrase is associated with a v...
research
∙
01/31/2021
Model-Based Testing of Networked Applications
We present a rigorous framework for automatically testing application-la...
research
∙
10/08/2020
Testing Differential Privacy with Dual Interpreters
Applying differential privacy at scale requires convenient ways to check...
research
∙
05/31/2019
Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress)
We present "interaction trees" (ITrees), a general-purpose data structur...
research
∙
05/29/2019
Fuzzi: A Three-Level Logic for Differential Privacy
Curators of sensitive datasets sometimes need to know whether queries ag...
research
∙
11/29/2018
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
We present the first formal verification of a networked server implement...
research
∙
10/26/2018
Synthesizing Symmetric Lenses
Lenses are programs that can be run both "front to back" and "back to fr...
research
∙
02/02/2018
When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise
We propose a new formal criterion for secure compilation, giving strong ...
research
∙
10/19/2017
Formally Secure Compilation of Unsafe Low-Level Components (Extended Abstract)
We propose a new formal criterion for secure compilation, providing stro...
research
∙
10/09/2017
Synthesizing Bijective Lenses
Bidirectional transformations between different data representations occ...
research
∙
05/20/2017
