131 citations · 343 across the 15 of their papers we have counts for
10 papers · 1 filter
Synthesizing Trajectory Queries from Examples
Stephen Mell, Favyen Bastani, Steve Zdancewic +1
Data scientists often need to write programs to process predictions of machine learning models, such as object detections and trajectories in video data. However, writing such quer…
Optimal Program Synthesis via Abstract Interpretation
Stephen Mell, Steve Zdancewic, Osbert Bastani
We consider the problem of synthesizing programs with numerical constants that optimize a quantitative objective, such as accuracy, over a set of input-output examples. We propose…
Ideograph: A Language for Expressing and Manipulating Structured Data
Stephen Mell, Osbert Bastani, Steve Zdancewic
We introduce Ideograph, a language for expressing and manipulating structured data. Its types describe kinds of structures, such as natural numbers, lists, multisets, binary trees,…
An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
Yannick Zakowski, Paul He, Chung-Kil Hur +1
Coinductive reasoning about infinitary structures such as streams is widely applicable. However, practical frameworks for developing coinductive proofs and finding reasoning princi…
Interaction Trees: Representing Recursive and Impure Programs in Coq
Li-yao Xia, Yannick Zakowski, Paul He +4
"Interaction trees" (ITrees) are a general-purpose data structure for representing the behaviors of recursive programs that interact with their environments. A coinductive variant…
A HoTT Quantum Equational Theory (Extended Version)
Jennifer Paykin, Steve Zdancewic
This paper presents an equational theory for the QRAM model of quantum computation, formulated as an embedded language inside of homotopy type theory. The embedded language approac…
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li +6
We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie toge…
Synthesizing Symmetric Lenses
Anders Miltner, Solomon Maina, Kathleen Fisher +3
Lenses are programs that can be run both "front to back" and "back to front," allowing updates to either their source or their target data to be transferred in both directions. Len…
Structural Operational Semantics for Control Flow Graph Machines
Dmitri Garbuzov, William Mansky, Christine Rizkallah +1
Compilers use control flow graph (CFG) representations of low-level programs because they are suited to program analysis and optimizations. However, formalizing the behavior and me…
Synthesizing Bijective Lenses
Anders Miltner, Kathleen Fisher, Benjamin C. Pierce +2
Bidirectional transformations between different data representations occur frequently in modern software systems. They appear as serializers and deserializers, as database views an…