Linear dependent types for differential privacy

DOI10.1145/2429069.2429113MaRDI QIDQ2931812zbMATH OpenOpenAlexFDO

Authors Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, Benjamin C. Pierce

Publication date 27 November 2014

Published in Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2429069.2429113

zbMATH Keywords

dependent typesdifferential privacylinear logictype systems

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Database theory (68P15)

Recommendations

• Distance makes the types grow stronger: a calculus for differential privacy
• Probabilistic relational reasoning for differential privacy
• LightDP: towards automating differential privacy proofs
• Formal verification of differential privacy for interactive systems (extended abstract)
• scientific article; zbMATH DE number 7333242

Cited in

(24)

• Resourceful program synthesis from graded linear types
• Generalized bounded linear logic and its categorical semantics
• Coupled relational symbolic execution for differential privacy
• Graded modal dependent type theory
• Model checking differentially private properties
• I got plenty o' nuttin'
• Combining Differential Privacy and Mutual Information for Analyzing Leakages in Workflows
• Relational cost analysis in a functional-imperative setting
• Preserving differential privacy under finite-precision semantics
• Distance makes the types grow stronger: a calculus for differential privacy
• Differential privacy in probabilistic systems
• LightDP: towards automating differential privacy proofs
• Generalized differential privacy: regions of priors that admit robust optimal mechanisms
• Formal verification of differential privacy for interactive systems (extended abstract)
• Divergences on monads for relational program logics
• Bunched Fuzz: sensitivity for vector metrics
• Certifying private probabilistic mechanisms
• Deriving distributive laws for graded linear types
• A partial metric semantics of higher-order types and approximate program transformations
• Tropical mathematics and the lambda-calculus I: metric and differential analysis of effectful programs
• Unifying graded linear logic and differential operators
• A linear type system for L^p-metric sensitivity analysis
• A Curry-Howard correspondence for linear, reversible computation
• A mixed linear and graded logic: proofs, terms, and models

Describes a project that uses

Uses Software

• z3

This page was built for publication: Linear dependent types for differential privacy

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2931812)