Sensitivity by Parametricity
summary
A method reduces proving a function’s sensitivity to ordinary type-checking by encoding metric relations at the type level and exploiting parametric polymorphism; the paper formalizes a calculus, proves soundness with logical relations, and shows sensitivity K corresponds to a type from Real D A to Real (KD) B. An embedded DSL and the Spar library (under 500 LOC, Haskell) checks examples like map, fold, fixed-length vectors and k‑means using the L1 norm*, uses rationals for scale, and requires termination.
AI-written summary · about
chapters (11)
- 0:00Differential privacy intro
- 1:05Laplace mechanism basics
- 2:10Formal sensitivity definition
- 3:55Automatic sensitivity via parametricity
- 5:19Type-level distance in Spar
- 6:23Parametricity and sensitivity types
- 7:25Sensitivity and differential privacy
- 8:08Advantages and limitations
- 9:39Soundness proof and formalization
- 11:49Key takeaways and future
- 13:13Q&A
related talks
24mDependent Coeffects for Local Sensitivity Analysis
25mPeter's early work on parametricity, and why it still matters to me
22mA Categorical Basis for Robust Program Analysis
49mSemantic Foundations for Probabilistic Programming
18mSpace-Efficient Polymorphic Gradual Typing, Mostly Parametric
42mProgramming with Math
01h 08mType Arithmetic and the Yoneda Lemma
14mType-Sensitive Algebraic Macros