Relational Cost Analysis for Functional-Imperative Programs
Relational cost analysis aims at formally establishing bounds on the difference in the evaluation costs of two programs. As a particular case, one can also use relational cost analysis to establish bounds on the difference in the evaluation cost of the same program on two different inputs. One way to perform relational cost analysis is to use a relational type-and-effect system that supports reasoning about relations between two executions of two programs.
Building on this basic idea, we present a type-and-effect system, called ARel, for reasoning about the relative cost of array-manipulating, higher-order functional-imperative programs. The key ingredient of our approach is a new lightweight type refinement discipline that we use to track relations (differences) between two mutable arrays. This discipline combined with Hoare-style triples built into the types allows us to express and establish precise relative costs of several interesting programs which imperatively update their data. We have implemented ARel using ideas from bidirectional typechecking.
Tue 20 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00
Program Analysis & SynthesisResearch Papers at Aurora Borealis
Chair(s): Daniel Winograd-Cort Target Corp
|Relational Cost Analysis for Functional-Imperative Programs|
Weihao Qu University at Buffalo, SUNY, Marco Gaboardi University at Buffalo, SUNY, Deepak Garg Max Planck Institute for Software Systems
|Fuzzi: A Three-Level Logic for Differential Privacy|
Hengchu Zhang University of Pennsylvania, Edo Roth University of Pennsylvania, Andreas Haeberlen University of Pennsylvania, USA, Benjamin C. Pierce University of Pennsylvania, Aaron Roth University of Pennsylvania, USA
|Synthesizing Differentially Private Programs|
Calvin Smith University of Wisconsin - Madison, Aws Albarghouthi University of Wisconsin-Madison
|Synthesizing Symmetric Lenses|
Anders Miltner Princeton University, Solomon Maina University of Pennsylvania, Kathleen Fisher Tufts University, USA, Benjamin C. Pierce University of Pennsylvania, David Walker Princeton University, Steve Zdancewic University of PennsylvaniaPre-print