Sensitivity by ParametricityOOPSLA 2024 Distinguished Artifact Award
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 OctDisplayed 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 20mTalk | 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 20mTalk | 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 20mTalk | 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 20mTalk | 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 |