Academic Journal
A Linear Type System for L^p-Metric Sensitivity Analysis
| العنوان: | A Linear Type System for L^p-Metric Sensitivity Analysis |
|---|---|
| المؤلفون: | Sannier, Victor, Baillot, Patrick |
| المساهمون: | Victor Sannier and Patrick Baillot |
| بيانات النشر: | Schloss Dagstuhl – Leibniz-Zentrum für Informatik |
| سنة النشر: | 2024 |
| المجموعة: | DROPS - Dagstuhl Research Online Publication Server (Schloss Dagstuhl - Leibniz Center for Informatics ) |
| مصطلحات موضوعية: | 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. |
| نوع الوثيقة: | article in journal/newspaper conference object |
| وصف الملف: | application/pdf |
| اللغة: | English |
| Relation: | Is Part Of LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024); https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.12 |
| DOI: | 10.4230/LIPIcs.FSCD.2024.12 |
| الاتاحة: | https://doi.org/10.4230/LIPIcs.FSCD.2024.12 https://nbn-resolving.org/urn:nbn:de:0030-drops-203412 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.12 |
| Rights: | https://creativecommons.org/licenses/by/4.0/legalcode |
| رقم الانضمام: | edsbas.88FFDB7 |
| قاعدة البيانات: | BASE |
| DOI: | 10.4230/LIPIcs.FSCD.2024.12 |
|---|