Bunched Fuzz: Sensitivity for Vector Metrics
| Autor: | june wunder, Arthur Azevedo de Amorim, Patrick Baillot, Marco Gaboardi |
|---|---|
| Přispěvatelé: | Boston University [Boston] (BU), Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires (SYCOMORES), Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), This material is based upon work supported by the NSF under Grant No. 1845803 and 2040249. The third author was partially supported by the french Program 'Investissements d’avenir' (I-ULNE SITE / ANR-16-IDEX-0004 ULNE) managed by the National Research Agency., ANR-16-IDEX-0004,ULNE,ULNE(2016), Boston University [Boston] [BU], Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires [SYCOMORES], Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL] |
| Jazyk: | angličtina |
| Rok vydání: | 2023 |
| Předmět: | |
| Zdroj: | ESOP 2023-European Symposium on Programming ESOP 2023-European Symposium on Programming, Apr 2023, Paris, France. ⟨10.48550/arXiv.2202.01901⟩ Programming Languages and Systems ISBN: 9783031300431 |
| Popis: | Program sensitivity measures the distance between the outputs of a program when run on two related inputs. This notion, which plays a key role in areas such as data privacy and optimization, has been the focus of several program analysis techniques introduced in recent years. Among the most successful ones, we can highlight type systems inspired by linear logic, as pioneered by Reed and Pierce in the Fuzz programming language. In Fuzz, each type is equipped with its own distance, and sensitivity analysis boils down to type checking. In particular, Fuzz features two product types, corresponding to two different notions of distance: the tensor product combines the distances of each component by adding them, while the with product takes their maximum.In this work, we show that these products can be generalized to arbitrary $$L^p$$ L p distances, metrics that are often used in privacy and optimization. The original Fuzz products, tensor and with, correspond to the special cases $$L^1$$ L 1 and $$L^\infty $$ L ∞ . To ease the handling of such products, we extend the Fuzz type system with bunches—as in the logic of bunched implications—where the distances of different groups of variables can be combined using different $$L^p$$ L p distances. We show that our extension can be used to reason about quantitative properties of probabilistic programs. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|