Gradual Sensitivity Typing
Damian Arquez, Mat\'ias Toro, \'Eric Tanter

TL;DR
This paper introduces GSoul, a language supporting gradual sensitivity typing, enabling flexible, mixed static and dynamic sensitivity analysis, which simplifies reasoning about function sensitivity especially in recursive functions and differential privacy applications.
Contribution
It formalizes and prototypes gradual sensitivity typing, combining static and dynamic checks, and demonstrates its benefits for recursive functions and differential privacy.
Findings
Supports recursive functions with static and dynamic sensitivity checks
Ensures gradual guarantees and metric preservation
Prototype implementation for testing gradual sensitivity typing
Abstract
Reasoning about the sensitivity of functions with respect to their inputs has interesting applications in various areas, such as differential privacy. In order to check and enforce sensitivity, several approaches have been developed, notably sensitivity type systems. In these systems, sensitivity can be seen as an effect in the sense of type-and-effects systems as originally proposed by Gifford and Lucassen. Because type-and-effect systems can make certain useful programming patterns tedious or overly conservative, there is value in bringing the benefits of gradual typing to these disciplines in order to ease their adoption. In this work, we motivate, formalize, and prototype gradual sensitivity typing. The language GSoul supports both the unrestricted unknown sensitivity and bounded imprecision in the form of intervals. Gradual sensitivity typing allows programmers to smoothly evolve…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSecurity and Verification in Computing · Logic, programming, and type systems · Formal Methods in Verification
