2026-07-23T06:31:08Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20341 2024-07-05T06:20:34Z ddc:004 open_access

A Linear Type System for L^p-Metric Sensitivity Analysis Sannier, Victor Baillot, Patrick type system linear logic sensitivity vector metrics differential privacy lambda-calculus functional programming denotational semantics When working in optimisation or privacy protection, one may need to estimate the sensitivity of computer programs, i.e., the maximum multiplicative increase in the distance between two inputs and the corresponding two outputs. In particular, differential privacy is a rigorous and widely used notion of privacy that is closely related to sensitivity. Several type systems for sensitivity and differential privacy based on linear logic have been proposed in the literature, starting with the functional language Fuzz. However, they are either limited to certain metrics (L¹ and L^∞), and thus to the associated privacy mechanisms, or they rely on a complex notion of type contexts that does not interact well with operational semantics. We therefore propose a graded linear type system - inspired by Bunched Fuzz [{w}under et al., 2023] - called Plurimetric Fuzz that handles L^p vector metrics (for 1 ≤ p ≤ +∞), uses standard type contexts, gives reasonable bounds on sensitivity, and has good metatheoretical properties. We also provide a denotational semantics in terms of metric complete partial orders, and translation mappings from and to Fuzz. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Victor Sannier and Patrick Baillot 2024 Is Part Of LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2024.12 urn:nbn:de:0030-drops-203412 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.12 eng https://creativecommons.org/licenses/by/4.0/legalcode