Hello! 👋

I'm june, a PhD student working with Marco Gaboardi at Boston University.
Interested in programming languages, software verification, data privacy, concurrency, and web development.

want to get in contact? my email is: june@junewunder.com


Bunched Fuzz: Sensitivity for Vector Metrics
june wunder, Arthur Azevedo de Amorim, Patrick Baillot, Marco Gaboardi
European Symposium on Programming (ESOP), 2023
[Springer]   [arXiv]   [pdf]   [pdf (rendered w/ OpenDyslexic)]


Program sensitivity measures the distance between the outputs of a program when run on two related inputs. This notion, which plays a key role in areas such as data privacy and optimization, has been the focus of several program analysis techniques introduced in recent years. Among the most successful ones, we can highlight type systems inspired by linear logic, as pioneered by Reed and Pierce in the Fuzz programming language. In Fuzz, each type is equipped with its own distance, and sensitivity analysis boils down to type checking. In particular, Fuzz features two product types, corresponding to two different notions of distance: the tensor product combines the distances of each component by adding them, while the with product takes their maximum.

In this work, we show that these products can be generalized to arbitrary Lp distances, metrics that are often used in privacy and optimization. The original Fuzz products, tensor and with, correspond to the special cases L1 and L∞. To ease the handling of such products, we extend the Fuzz type system with bunches---as in the logic of bunched implications---where the distances of different groups of variables can be combined using different Lp distances. We show that our extension can be used to reason about quantitative properties of probabilistic programs.