Fri 25 Oct 2024 11:40 - 12:00 at Pasadena - Probabilistic Programming and Analysis 2 Chair(s): Xin Zhang

The work of Fuzz has pioneered the use of functional programming languages where types allow reasoning about the sensitivity of programs. Fuzz and subsequent work (e.g., DFuzz and Duet) use advanced technical devices like linear types, modal types, and partial evaluation. These features usually require the design of a new programming language from scratch–a significant task on its own! While these features are part of the classical toolbox of programming languages, they are often unfamiliar to non-experts in this field. Fortunately, recent studies (e.g., Solo) have shown that linear and complex types in general, are not strictly needed for the task of determining programs’ sensitivity since this can be achieved by annotating base types with static sensitivity information. In this work, we take a different approach. We propose to enrich base types with information about the metric relation between values, and we present the novel idea of applying parametricity, i.e., a well-known abstract uniformity property enjoyed by polymorphic functions, to derive direct proofs for the sensitivity of functions. A direct consequence of our result is that calculating and proving the sensitivity of functions is reduced to simply type-checking in a programming language with support for polymorphism and type-level naturals. We formalize our main result in a calculus, prove its soundness, and implement a software library in the programming language Haskell–where we reason about the sensitivity of canonical examples. We show that the simplicity of our approach allows us to exploit the type inference of the host language to support a limited form of sensitivity inference–something that to the best of our knowledge has not been previously explored. Furthermore, we extend the language with a privacy monad to showcase how our library can be used in practical scenarios such as the implementation of differentially private programs, where the privacy guarantees depend on the sensitivity of user-defined functions. Our library, called Spar, is implemented in less than 500 lines of code.

Fri 25 Oct

Displayed time zone: Pacific Time (US & Canada) change

11:00 - 12:20
Probabilistic Programming and Analysis 2OOPSLA 2024 at Pasadena
Chair(s): Xin Zhang Peking University
11:00
20m
Talk
Programmable MCMC with Soundly Composed Guide Programs
OOPSLA 2024
Long Pham Carnegie Mellon University, Di Wang Peking University, Feras Saad Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University
DOI
11:20
20m
Talk
Quantitative Bounds on Resource Usage of Probabilistic Programs
OOPSLA 2024
Krishnendu Chatterjee IST Austria, Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Tobias Meggendorfer Lancaster University, UK (Leipzig Campus), Đorđe Žikelić Singapore Management University, Singapore
DOI
11:40
20m
Talk
Sensitivity by ParametricityOOPSLA 2024 Distinguished Artifact Award
OOPSLA 2024
Elisabet Lobo-Vesga DPella AB, Carlos Tomé Cortiñas Chalmers University of Technology, Alejandro Russo Chalmers University of Technology, Sweden / University of Gothenburg, Sweden / DPella AB, Sweden, Marco Gaboardi Boston University
DOI
12:00
20m
Talk
Tachis: Higher-Order Separation Logic with Credits for Expected Costs
OOPSLA 2024
Philipp G. Haselwarter Aarhus University, Kwing Hei Li Aarhus University, Markus de Medeiros New York University, Simon Oddershede Gregersen New York University, Alejandro Aguirre Aarhus University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University
DOI Pre-print