Pith. sign in

REVIEW 3 major objections 4 minor 54 references

Duet: An Expressive Higher-order Language and Linear Type System for Statically Enforcing Differential Privacy

T0 review · 3 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Duet claims differential privacy can be enforced statically by a two-language linear type system, making privacy proofs for higher-order machine learning programs automatic.

desk verdict Genuinely novel two-language design for per-argument privacy accounting; the ML case studies overclaim a joint row-change guarantee the formal system does not provide. read the letter →

arxiv 1909.02481 v1 pith:NPLJK3VB submitted 2019-09-05 cs.PL cs.CR

Joseph P. Near , David Darais , Chike Abuah , Tim Stevens , Pranav Gaddamadugu , Lun Wang , Neel Somani , Mu Zhang
show 3 more authors
Nikhil Sharma Alex Shan Dawn Song
This is my paper · ORCID
classification cs.PLcs.CR
keywords differentialprivacylineartypesystemssoundnesshigher-orderprogrammingmachinelearningverificationRényizero-concentratedcosttracking
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Duet is a programming language and type system that aims to make differential privacy verification automatic for general-purpose, higher-order programs, not just hand-crafted queries. Its central claim is that any well-typed Duet program is guaranteed to satisfy the stated privacy bound for each of its sensitive arguments, with no manual privacy proof. The design splits the language into a sensitivity language, which tracks how much outputs can change, and a privacy language, which tracks how much privacy budget each argument spends. This split is what lets the system handle $(\epsilon,\delta)$-differential privacy and recent alternatives like Rényi and concentrated differential privacy, which earlier linear type systems could not express tightly. If the claim is right, privacy-sensitive machine learning code can be checked by a compiler rather than by a privacy expert.

What carries the argument

The load-bearing construction is the pair of mutually embedded linear type systems connected by a truncation operation. The sensitivity language annotates each variable with a non-negative real sensitivity and allows scaling; the privacy language annotates each variable with a privacy cost such as $(\epsilon,\delta)$ and forbids scaling, so that composition reflects the sequential-composition rule of the privacy definition rather than a linear scaling rule. Privacy lambdas are multi-argument and typed as $(\tau_1 @ p_1, \ldots, \tau_n @ p_n) \to^* \tau$, meaning the function provably consumes privacy cost $p_i$ for its $i$-th argument, and a box type captures a sensitivity context in the sensitivity language so the cost can be paid later. The Gaussian mechanism and its siblings are typing rules that convert a proved sensitivity bound into a privacy-cost annotation, which is how the system states privacy bounds without an effect monad.

What would settle it

Find a neighboring pair of datasets on which the built-in L2 gradient primitive changes by more than its assumed 1-Lipschitz bound, or a pair on which the sampling primitive's privacy-amplification lemma fails; then some well-typed Duet program would violate its claimed $(\epsilon,\delta)$ privacy in a direct measurement of output distributions.

Watch

Extended reading notes

Core claim

The paper establishes a type-soundness theorem for Duet: any well-typed term has a denotation that inhabits the interpretation of its typing context, and as a corollary every well-typed privacy $\lambda$ satisfies $(\epsilon,\delta)$-differential privacy (or the corresponding variant for Rényi, zero-concentrated, or truncated-concentrated differential privacy) independently for each argument. The technical discovery is that linear typing with scaling is the right model for function sensitivity, while linear typing without scaling is the right model for privacy cost: $(\epsilon,\delta)$-differential privacy does not scale linearly, so allowing scaling forces the suboptimal group-privacy bound and gives worse results. Duet therefore restricts the privacy language to 1-sensitive arguments and uses truncation to move between the two languages, encoding the Gaussian mechanism and its relatives as the interface. This is enough to verify private stochastic gradient descent, private Frank-Wolfe, gradient clipping, adaptive clipping, and hyperparameter tuning, with inferred bounds equal to or better than previously published manual proofs.

Load-bearing premise

The verified privacy bounds for the machine-learning cases depend on the built-in primitives for gradient, clipping, conversion, and sampling actually having the sensitivity and privacy properties their type signatures claim, and the paper states that these low-level mechanisms are opaque and trusted, so an incorrect signature would void the bounds.

Editorial extensions

If this is right

  • Well-typed Duet programs get a machine-checked privacy bound for free: a guarantee that previously required a bespoke expert proof is now a typing judgment.
  • The same program can be checked under $(\epsilon,\delta)$-DP, Rényi DP, zCDP, and tCDP, with bounds tight enough to match or improve on the best manual analyses for private SGD and Frank-Wolfe.
  • Privacy costs are tracked independently for multiple arguments, so a program that applies a mechanism to two different inputs is not forced to pay the sum for each; double-charging happens only when the same variable feeds both arguments.
  • Privacy variants can be mixed in one program, such as an $\epsilon$-DP Laplace step inside a zCDP loop, with automatic conversion to a single $(\epsilon,\delta)$ report.
  • The typechecker runs in sub-millisecond to a few milliseconds on the case studies, so privacy checking could be part of ordinary compilation.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The paper's co-effect treatment of privacy cost (tracked per variable in the context, rather than as an effect on the output) suggests a general recipe for other relational properties that do not compose by scaling, such as robustness or fairness metrics: keep the property in a no-scaling linear language and pair it with a scaling sensitivity language, connecting them by a truncation-like interfac
  • Because the privacy language does not support currying, the design predicts that any extension to full currying in the privacy language would either reintroduce suboptimal group-privacy bounds or require a different way of combining per-argument costs; testing this boundary would clarify the limits of the approach.
  • A natural next step is to mechanize the soundness proof in a proof assistant, removing the last hand-checked part of the chain; the proof is by induction and appeals to standard composition theorems, so the barrier is mostly engineering.
  • The trusted-primitive bottleneck could be addressed by a second, lower-level verifier for the primitive implementations; if such a verifier existed, the end-to-end guarantee would no longer rely on unverified assumptions about gradient, clipping, and sampling.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper presents Duet, a higher-order programming language with two mutually embedded linear type systems: a sensitivity language (linear types with metric scaling, following Fuzz/DFuzz) and a privacy language (linear types without scaling) for enforcing differential privacy. The privacy language supports (ε,δ)-DP, Rényi DP, zero-concentrated CDP, and truncated concentrated CDP, with mechanisms such as Gaussian noise as the interface between the two languages. The central metatheoretic claim is a soundness theorem: every well-typed privacy lambda satisfies the relevant privacy property independently for each of its arguments. The paper further claims that this system can automatically verify realistic machine learning algorithms—noisy gradient descent, private Frank-Wolfe, minibatching, adaptive clipping, and others—with privacy bounds that match or improve on prior manual proofs, and it reports an implementation and accuracy experiments on several datasets.

Significance. If the soundness theorem and the case-study claims are correct, Duet is a significant advance in language-based differential privacy: it is among the first systems to combine higher-order programming, multiple recent DP variants, and independent privacy accounting for multiple arguments in a single automated type system. The design idea of using a non-scalable linear privacy language embedded in a scalable sensitivity language is elegant and well motivated, and the contextual-modal box construct for deferring sensitivity costs is a useful contribution. The paper also ships an open-source implementation, reports very fast typechecking times, and provides concrete case studies with stated privacy bounds, which makes the claims reproducible and testable. The main value of the paper hinges on whether the advertised machine-learning privacy bounds actually follow from the soundness theorem; on that point I have a serious concern, detailed below.

major comments (3)
  1. [§3.6, §5.1, §5.4] The soundness theorem gives only a per-argument guarantee, but the headline case studies compare against manual proofs that use one-row neighbors changing both the feature matrix and the label matrix simultaneously. The definition of (D1@p1,...,Dn@pn) ⊸∗ X in §3.6 varies each argument one at a time while holding the others fixed, and the corollary of Theorem 3.1 is explicitly stated as '(ε,δ)-differential privacy ... independently for each of its arguments.' In §5.1 and §5.4, noisy-gradient-descent and minibatch-gradient-descent pass X and y as separate privacy arguments with identical annotations and then claim bounds 'equivalent to the manual proof of Bassily et al.' In that manual proof a neighboring database changes one row, i.e., both X and y change at once. The per-argument guarantee does not cover a simultaneous change of two context variables; under the product metric implicit in the semantics, a joint row change costs the sum of the individual costs. Moreover, the MGauss rule in Figure 6 checks the body's sensitivity only in each listed variable separately, so it does not certify the joint sensitivity needed for the Gaussian mechanism on a combined (X,y) argument. Consequently, the advertised equivalence with Bassily et al. for SGD, Frank-Wolfe, and minibatching is not entailed by the formal system as presented. The authors should either reformulate the case studies so that the sensitive database is a single argument with a metric that models one-row (X,y) changes, or explicitly weaken the case-study claims to per-argument privacy.
  2. [Figure 4, Loop rule; Appendix C, Theorem C.2] The Loop rule uses the advanced composition bound 2ϵ√(2n ln(1/δ′)) without the side conditions needed by the theorem it cites. The premise types e1 : R+[δ′], which permits δ′=0, but ln(1/0) is undefined as a privacy parameter. The rule therefore types programs whose formal privacy bound is not meaningful. Relatedly, Theorem C.2 in the appendix states the composed bound as ˆϵ = e^(2ϵ_i√(2n log(1/δ′))) (as printed), while the typing rule and the Loop proof case use 2ϵ√(2n ln(1/δ′)) without the exponential. Please state the exact theorem being used, with all required side conditions (e.g., δ′>0, n≥1), and make the appendix statement and the typing rule consistent.
  3. [Appendix D] The proof of Theorem 3.1 covers only 'key cases' and describes the remaining typing rules as 'straightforward adaptations.' Since the paper's contributions include the soundness of sample, pfld-rows, above-threshold, exponential, and the conversion rules used in the case studies, the formal claim is incomplete in this version for those rules. Either provide a complete induction or state explicitly that those rules are proved only in the extended version and mark the affected case-study claims as conditional on that proof.
minor comments (4)
  1. [§2.1] The informal statement of advanced composition says 'for 0 < ε′ < 1 and δ′ > 0,' but the formula and the later typing rule do not enforce or use that condition; please harmonize the informal statement with the theorem actually used.
  2. [References] References [13] and [14] are the same paper (Bassily, Smith, and Thakurta, 'Private empirical risk minimization'); please renumber and deduplicate.
  3. [§4.2 and §5.4] The sample rule in Figure 6 encodes the loose amplification bound (2m2ε1/m1, m2δ1/m1), and Section 5.4 acknowledges that this bound is loose. The abstract and introduction describe the case-study bounds as 'optimal or near-optimal'; please qualify this language to account for the loose amplification used in the minibatching case study.
  4. [Figure 4 and Figure 6] The typing rules rely heavily on color to distinguish the sensitivity and privacy languages; even with the colorblind-friendly palette, this can be ambiguous in greyscale printing. Consider adding a non-color distinguishing convention, such as different arrow symbols or syntactic markers.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the verified privacy bounds are sound applications of standard, externally cited DP theorems via a type system, with no fitted parameters or load-bearing self-citations.

full rationale

The paper's derivation chain is a compositional type-soundness argument, not a fitted or self-referential prediction. The privacy typing judgment is interpreted semantically in Section 3.6 as exactly the per-argument differential-privacy definition, and Theorem D.1 (Soundness) proves by induction that each typing rule is sound. The key proof cases for Bind, MGauss, and Loop invoke external theorems (Dwork-Roth for Gaussian and advanced composition; Mironov for RDP; Bun-Steinke for zCDP; Bun et al. for tCDP), and these are cited as prior literature, not derived from Duet itself. The case-study bounds in Section 5 (e.g., the Bassily et al. matching bounds in Sections 5.1 and 5.4) are outputs of fixed typing rules; no parameter is fitted to those manual results, and the manual bounds are not used to adjust or justify the rules after the fact. The only trust assumptions are the primitive signatures in Figure 6 (Lipschitz gradients, clipping, sampling amplification), which the paper explicitly labels as opaque and trusted (Section 2.3); whether those signatures are correct is an assumption-validity concern, not a circularity. The self-citations in the references ([32], [33]) appear only as related work on differentially private SQL and play no role in the soundness argument. Accordingly, no step in the paper's claimed derivation reduces to its own inputs by construction.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

No free parameters are fitted to data in the statistics sense; type-level variables (ε, δ, ρ) are program parameters supplied by the user. The central claim rests on standard differential privacy theorems, termination, and trusted primitive types.

assumptions (4)
  • domain assumption Standard differential privacy theorems: Gaussian mechanism, advanced composition, sequential composition, privacy amplification by subsampling, conversions between DP variants.
    Invoked in Appendix C and in typing rules for gauss, loop, sample, and ZCDP conversion. These are external mathematical results the soundness proof relies on.
  • domain assumption All Duet programs terminate (no general recursion).
    Section 3.6: 'Every term in our language terminates by design.' This is needed for the total metric-space semantics and for sound sensitivity types.
  • domain assumption Trusted primitive signatures for matrix operations and mechanisms: gradient, clip, conv, sample, above-threshold have the sensitivity and privacy types in Figure 6.
    Section 2.3 states low-level mechanisms are opaque and trusted. The case-study privacy bounds rely on these signatures being correct.
  • standard math Metric-space model of types a la Fuzz, including the discrete metric for the data type and row-wise matrix norms.
    Section 3.6 and Appendix D use metric spaces to interpret types; this is standard semantics for sensitivity analysis, imported from prior work.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Duet: An Expressive Higher-order Language and Linear Type System for Statically Enforcing Differential Privacy." pith.science (2026). https://pith.science/paper/NPLJK3VB

@misc{pith2026190902481,
  author       = {Pith},
  title        = {Pith review of: Duet: An Expressive Higher-order Language and Linear Type System for Statically Enforcing Differential Privacy},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/NPLJK3VB}},
  note         = {Machine review of arXiv:1909.02481}
}
read the original abstract

During the past decade, differential privacy has become the gold standard for protecting the privacy of individuals. However, verifying that a particular program provides differential privacy often remains a manual task to be completed by an expert in the field. Language-based techniques have been proposed for fully automating proofs of differential privacy via type system design, however these results have lagged behind advances in differentially-private algorithms, leaving a noticeable gap in programs which can be automatically verified while also providing state-of-the-art bounds on privacy. We propose Duet, an expressive higher-order language, linear type system and tool for automatically verifying differential privacy of general-purpose higher-order programs. In addition to general purpose programming, Duet supports encoding machine learning algorithms such as stochastic gradient descent, as well as common auxiliary data analysis tasks such as clipping, normalization and hyperparameter tuning - each of which are particularly challenging to encode in a statically verified differential privacy framework. We present a core design of the Duet language and linear type system, and complete key proofs about privacy for well-typed programs. We then show how to extend Duet to support realistic machine learning applications and recent variants of differential privacy which result in improved accuracy for many practical differentially private algorithms. Finally, we implement several differentially private machine learning algorithms in Duet which have never before been automatically verified by a language-based tool, and we present experimental results which demonstrate the benefits of Duet's language design in terms of accuracy of trained machine learning models.

Figures

Figures reproduced from arXiv: 1909.02481 by the authors.

Figure 1
Figure 1. Variants of Differential Privacy its input by 1 has the effect of increasing or decreasing its output by 2. A real-valued function f is called n-sensitive if maxx,y:|x−y | ≤1 |f (x) − f (y)| = n. This idea can be generalized to vector-valued functions. The global L1 sensitivity of a query f : D n → R d is written GSf and defined GSf = maxx,y:d(x,y)=1 |f (x) − f (y)|1 where | − |1 is the L1 norm (i.e., sum of pointwi… view at source ↗
Figure 2
Figure 2. Legend: SA = capable of sensitivity analysis; HO = support for higher order programming, program composition, and compound datatypes; DT = support for dependently typed privacy bounds; MA = support for distinct privacy bounds of multiple input arguments; Rel-ext = supports extensions to support non-differential-privacy relations; ϵ-DP = supports ϵ￾differential-privacy; (ϵ, δ )-DP = supports (ϵ, δ )-differential-priv… view at source ↗
Figure 3
Figure 3. Core Types and Terms 3.3 Duet Syntax & Typing Rules [PITH_FULL_IMAGE:figures/full_fig_p014_3.png] view at source ↗
Figures from the paper (21 more)
Figure 4
Figure 4. Figure 4: Core Typing Rules this paper. Because the typelevel representation of a natural number can be a variable, its value is therefore not statically determined, rather it is statically tracked via typelevel symbolic formulas. Type contexts in the sensitivity language Γs tra…
Figure 5
Figure 5. Figure 5: Distance Metrics for Matrices Distance is the number of rows on which X and X ′ differ; commonly used to describe neighboring input datasets. Ex. 2: |X − X ′ |MU L1 [m, n] R = Í i Í j |Xi,j − X ′ i,j |R Distance is the sum of elementwise differences. Ex. 3: |X − X ′ |M…
Figure 6
Figure 6. Figure 6: Matrix Typing Rules than 1: clipc xi ≜  xi ∥xi ∥c if ∥xi ∥c > 1 xi if ∥xi ∥c ≤ 1 The clipping process is encoded in Duet as clip ( [PITH_FULL_IMAGE:figures/full_fig_p021_6.png]
Figure 7
Figure 7. Figure 7: Summary of Typechecking Performance on Case [PITH_FULL_IMAGE:figures/full_fig_p027_7.png]
Figure 8
Figure 8. Figure 8: Dataset Used in Accuracy Evalu￾ation We present the results in [PITH_FULL_IMAGE:figures/full_fig_p027_8.png]
Figure 9
Figure 9. Figure 9: Accuracy Results for Noisy Gradient Descent (Top) and Noisy Frank-Wolfe (Bottom). [PITH_FULL_IMAGE:figures/full_fig_p028_9.png]
Figure 10
Figure 10. Figure 10: Types and Kinds (shared) [PITH_FULL_IMAGE:figures/full_fig_p035_10.png]
Figure 11
Figure 11. Figure 11: Type Metafunctions [PITH_FULL_IMAGE:figures/full_fig_p036_11.png]
Figure 12
Figure 12. Figure 12: Sensitivity and Privacy Languages [PITH_FULL_IMAGE:figures/full_fig_p037_12.png]
Figure 13
Figure 13. Figure 13: Sensitivity and Privacy Metafunctions [PITH_FULL_IMAGE:figures/full_fig_p038_13.png]
Figure 14
Figure 14. Figure 14: Kinding and Type Formation [PITH_FULL_IMAGE:figures/full_fig_p039_14.png]
Figure 15
Figure 15. Figure 15: Sensitivity Typing—Literals and Arithmetic [PITH_FULL_IMAGE:figures/full_fig_p040_15.png]
Figure 16
Figure 16. Figure 16: Sensitivity Typing—Matrices [PITH_FULL_IMAGE:figures/full_fig_p041_16.png]
Figure 17
Figure 17. Figure 17: Sensitivity Typing—Iteration and Connectives [PITH_FULL_IMAGE:figures/full_fig_p042_17.png]
Figure 18
Figure 18. Figure 18: Privacy Type Systems [PITH_FULL_IMAGE:figures/full_fig_p043_18.png]
Figure 19
Figure 19. Figure 19: Metrics (1) [PITH_FULL_IMAGE:figures/full_fig_p044_19.png]
Figure 20
Figure 20. Figure 20: Metrics (2) [PITH_FULL_IMAGE:figures/full_fig_p045_20.png]
Figure 21
Figure 21. Figure 21: Semantics of Typing [PITH_FULL_IMAGE:figures/full_fig_p046_21.png]
Figure 22
Figure 22. Figure 22: Privacy Type System Modifications, Rényi Differential Privacy [PITH_FULL_IMAGE:figures/full_fig_p054_22.png]
Figure 23
Figure 23. Figure 23: Privacy Type System Modifications, Zero-Concentrated Differential Privacy [PITH_FULL_IMAGE:figures/full_fig_p056_23.png]
Figure 24
Figure 24. Figure 24: Privacy Type System Modifications, Truncated Concentrated Differential Privacy [PITH_FULL_IMAGE:figures/full_fig_p059_24.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

54 extracted references · 44 canonical work pages

  1. [1]

    [n. d.]. Apple previews iOS 10, the biggest iOS release ever. http://www.apple.com/newsroom/2016/06/ apple-previews-ios-10-biggest-ios-release-ever.html

    work page 2016

  2. [2]

    scikit-learn: Standardization, or mean removal and variance scaling

    2019. scikit-learn: Standardization, or mean removal and variance scaling. https://scikit-learn.org/stable/modules/ preprocessing.html#preprocessing-scaler

    work page 2019

  3. [3]

    Martin Abadi, Andy Chu, Ian Goodfellow, H Brendan McMahan, Ilya Mironov, Kunal Talwar, and Li Zhang. 2016. Deep learning with differential privacy. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. ACM, 308–318

    work page 2016

  4. [4]

    Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. 2017. A semantic account of metric preservation. In POPL, Vol. 52. ACM, 545–556

    work page 2017

  5. [5]

    Andrew Barber. 1996. Dual Intuitionistic Linear Logic . Technical Report ECS-LFCS-96-347. University of Edinburgh

    work page 1996

  6. [6]

    Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesus Gallego Arias, Andy Gordon, Justin Hsu, and Pierre-Yves Strub. 2016. Differentially Private Bayesian Programming. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS ’16) . ACM, New York, NY, USA, 68–79. https://doi.org/10.1145/2976749. 2978371

    doi:10.1145/2976749 2016

  7. [7]

    Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016. Advanced probabilistic couplings for differential privacy. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. ACM, 55–67

    work page 2016

  8. [8]

    Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, and Pierre-Yves Strub. 2015. Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. In POPL. ACM, 55–68

    work page 2015

Show all 54 references
  1. [9]

    Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016. Proving differential privacy via probabilistic couplings. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science . ACM, 749–758

    2016

  2. [10]

    Gilles Barthe, Marco Gaboardi, Justin Hsu, and Benjamin Pierce. 2016. Programming language techniques for differential privacy. ACM SIGLOG News 3, 1 (2016), 34–53

    2016

  3. [11]

    Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella-Béguelin. 2013. Probabilistic relational reasoning for differential privacy. ACM Transactions on Programming Languages and Systems (TOPLAS) 35, 3 (2013), 9

    2013

  4. [12]

    Gilles Barthe and Federico Olmedo. 2013. Beyond differential privacy: Composition theorems and relational logic for f-divergences between probabilistic programs. In International Colloquium on Automata, Languages, and Programming . Springer, 49–60

    2013

  5. [14]

    Raef Bassily, Adam Smith, and Abhradeep Thakurta. 2014. Private empirical risk minimization: Efficient algorithms and tight error bounds. In Foundations of Computer Science (FOCS), 2014 IEEE 55th Annual Symposium on . IEEE, 464–473

    2014

  6. [15]

    Mark Bun, Cynthia Dwork, Guy N Rothblum, and Thomas Steinke. 2018. Composable and versatile privacy via truncated CDP. In Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing . ACM, 74–86

    2018

  7. [16]

    Mark Bun and Thomas Steinke. 2016. Concentrated differential privacy: Simplifications, extensions, and lower bounds. In Theory of Cryptography Conference . Springer, 635–658

    2016

  8. [17]

    Kamalika Chaudhuri, Claire Monteleoni, and Anand D Sarwate. 2011. Differentially private empirical risk minimization. Journal of Machine Learning Research 12, Mar (2011), 1069–1109

    2011

  9. [18]

    Kamalika Chaudhuri and Staal A Vinterbo. 2013. A stability-based validation procedure for differentially private machine learning. In Advances in Neural Information Processing Systems . 2652–2660

    2013

  10. [19]

    Ezgi Çiçek, Weihao Qu, Gilles Barthe, Marco Gaboardi, and Deepak Garg. 2018. Bidirectional Type Checking for Relational Properties. CoRR abs/1812.05067 (2018). arXiv:1812.05067 http://arxiv.org/abs/1812.05067

    2018 arXiv

  11. [20]

    Arthur Azevedo De Amorim, Marco Gaboardi, Emilio Jesús Gallego Arias, and Justin Hsu. 2014. Really Natural Linear Indexed Type Checking. In Proceedings of the 26nd 2014 International Symposium on Implementation and Application of Functional Languages. ACM, 5

    2014

  12. [21]

    Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, and Shin-ya Katsumata. 2018. Metric Semantics for Probabilistic Relational Reasoning. CoRR abs/1807.05091 (2018). arXiv:1807.05091 http://arxiv.org/abs/1807.05091

    2018 arXiv

  13. [22]

    Cynthia Dwork. 2006. Differential Privacy. In Automata, Languages and Programming, Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener (Eds.). Lecture Notes in Computer Science, Vol. 4052. Springer Berlin Heidelberg, 1–12. https://doi.org/10.1007/11787006_1

    2006 doi

  14. [23]

    Cynthia Dwork and Jing Lei. 2009. Differential privacy and robust statistics. In Proceedings of the forty-first annual ACM symposium on Theory of computing . ACM, 371–380

    2009

  15. [24]

    Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam Smith. 2006. Calibrating noise to sensitivity in private data analysis. In Theory of Cryptography Conference . Springer, 265–284. 30 Joseph P. Near, David Darais, Chike Abuah, Tim Stevens, Pranav Gaddamadugu, Lun Wang, Neel...

    2006

  16. [25]

    Cynthia Dwork, Aaron Roth, et al. 2014. The algorithmic foundations of differential privacy. Foundations and Trends® in Theoretical Computer Science 9, 3–4 (2014), 211–407

    2014

  17. [26]

    Úlfar Erlingsson, Vasyl Pihur, and Aleksandra Korolova. 2014. Rappor: Randomized aggregatable privacy-preserving ordinal response. In Proceedings of the 2014 ACM SIGSAC conference on computer and communications security . ACM, 1054–1067

    2014

  18. [27]

    Matt Fredrikson, Somesh Jha, and Thomas Ristenpart. 2015. Model Inversion Attacks That Exploit Confidence Information and Basic Countermeasures. In Proceedings of the 22Nd ACM SIGSAC Conference on Computer and Communications Security (CCS ’15) . ACM, New York, NY, USA, 1322–13...

    2015

  19. [28]

    Arik Friedman, Shlomo Berkovsky, and Mohamed Ali Kaafar. 2016. A differential privacy framework for matrix factorization recommender systems. User Modeling and User-Adapted Interaction 26, 5 (2016), 425–458

    2016

  20. [29]

    Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C Pierce. 2013. Linear dependent types for differential privacy. In POPL, Vol. 48. ACM, 357–370

    2013

  21. [30]

    Jean-Yves Girard. 1987. Linear Logic. Theor. Comput. Sci. 50, 1 (Jan. 1987), 1–102. https://doi.org/10.1016/0304-3975(87) 90045-4

    1987 doi

  22. [31]

    Samuel Haney, Ashwin Machanavajjhala, John M Abowd, Matthew Graham, Mark Kutzbach, and Lars Vilhuber. 2017. Utility cost of formal privacy for releasing national employer-employee statistics. In Proceedings of the 2017 ACM International Conference on Management of Data . ACM, ...

    2017

  23. [32]

    Noah Johnson, Joseph P Near, and Dawn Song. 2018. Towards practical differential privacy for SQL queries.Proceedings of the VLDB Endowment 11, 5 (2018), 526–539

    2018

  24. [33]

    Johnson, Joseph P

    Noah M. Johnson, Joseph P. Near, and Dawn Xiaodong Song. 2017. Towards Practical Differential Privacy for SQL Queries. CoRR abs/1706.09479 (2017). http://arxiv.org/abs/1706.09479

    2017 arXiv

  25. [34]

    Ashwin Machanavajjhala, Daniel Kifer, John Abowd, Johannes Gehrke, and Lars Vilhuber. 2008. Privacy: Theory meets practice on the map. In Proceedings of the 2008 IEEE 24th International Conference on Data Engineering . IEEE Computer Society, 277–286

    2008

  26. [35]

    Frank McSherry and Kunal Talwar. 2007. Mechanism design via differential privacy. In Foundations of Computer Science, 2007. FOCS’07. 48th Annual IEEE Symposium on . IEEE, 94–103

    2007

  27. [37]

    Frank D McSherry. 2009. Privacy integrated queries: an extensible platform for privacy-preserving data analysis. In Proceedings of the 2009 ACM SIGMOD International Conference on Management of data . ACM, 19–30

    2009

  28. [38]

    Ilya Mironov. 2017. Renyi differential privacy. In Computer Security Foundations Symposium (CSF), 2017 IEEE 30th . IEEE, 263–275

    2017

  29. [39]

    Prashanth Mohan, Abhradeep Thakurta, Elaine Shi, Dawn Song, and David Culler. 2012. GUPT: privacy preserving data analysis made easy. In Proceedings of the 2012 ACM SIGMOD International Conference on Management of Data . ACM, 349–360

    2012

  30. [40]

    Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 2008. Contextual Modal Type Theory.ACM Trans. Comput. Logic 9, 3, Article 23 (June 2008), 49 pages. https://doi.org/10.1145/1352582.1352591

    2008

  31. [41]

    Arjun Narayan and Andreas Haeberlen. 2012. DJoin: differentially private join queries over distributed databases. In Presented as part of the 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI 12) . 149–162

    2012

  32. [42]

    Nicolas Papernot, Martín Abadi, Ulfar Erlingsson, Ian Goodfellow, and Kunal Talwar. 2016. Semi-supervised knowledge transfer for deep learning from private training data. arXiv preprint arXiv:1610.05755 (2016)

    2016 arXiv

  33. [43]

    Davide Proserpio, Sharon Goldberg, and Frank McSherry. 2014. Calibrating data to sensitivity in private data analysis: A platform for differentially-private analysis of weighted datasets. PVLDB 7, 8 (2014), 637–648

    2014

  34. [44]

    Jason Reed and Benjamin C Pierce. 2010. Distance makes the types grow stronger: a calculus for differential privacy. ICFP 45, 9 (2010), 157–168

    2010

  35. [45]

    Indrajit Roy, Srinath TV Setty, Ann Kilzer, Vitaly Shmatikov, and Emmett Witchel. 2010. Airavat: Security and Privacy for MapReduce.. In NSDI, Vol. 10. 297–312

    2010

  36. [46]

    Tetsuya Sato. 2016. Approximate relational Hoare logic for continuous random samplings.Electronic Notes in Theoretical Computer Science 325 (2016), 277–298

    2016

  37. [47]

    Tetsuya Sato, Gilles Barthe, Marco Gaboardi, Justin Hsu, and Shin-ya Katsumata. 2019. Approximate span liftings: Compositional semantics for relaxations of differential privacy. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, 1–14

    2019

  38. [48]

    Shokri and V

    R. Shokri and V. Shmatikov. 2015. Privacy-preserving deep learning. In 2015 53rd Annual Allerton Conference on Communication, Control, and Computing (Allerton) . 909–910. https://doi.org/10.1109/ALLERTON.2015.7447103

    2015

  39. [49]

    Shokri, M

    R. Shokri, M. Stronati, C. Song, and V. Shmatikov. 2017. Membership Inference Attacks Against Machine Learning Models. In 2017 IEEE Symposium on Security and Privacy (SP) . 3–18. https://doi.org/10.1109/SP.2017.41 Duet: An Expressive Higher-order Language and Linear Type Syste...

    2017 doi

  40. [50]

    Shuang Song, Kamalika Chaudhuri, and Anand D Sarwate. 2013. Stochastic gradient descent with differentially private updates. In Global Conference on Signal and Information Processing (GlobalSIP), 2013 IEEE . IEEE, 245–248

    2013

  41. [51]

    Kunal Talwar, Abhradeep Guha Thakurta, and Li Zhang. 2015. Nearly optimal private lasso. In Advances in Neural Information Processing Systems. 3025–3033

    2015

  42. [52]

    Yu-Xiang Wang, Borja Balle, and Shiva Kasiviswanathan. 2018. Subsampled Rényi Differential Privacy and Analytical Moments Accountant. CoRR abs/1808.00087 (2018). arXiv:1808.00087 http://arxiv.org/abs/1808.00087

    2018 arXiv

  43. [53]

    X. Wu, M. Fredrikson, S. Jha, and J. F. Naughton. 2016. A Methodology for Formalizing Model-Inversion Attacks. In 2016 IEEE 29th Computer Security Foundations Symposium (CSF) . 355–370. https://doi.org/10.1109/CSF.2016.32

    2016 doi

  44. [54]

    Xi Wu, Fengan Li, Arun Kumar, Kamalika Chaudhuri, Somesh Jha, and Jeffrey Naughton. 2017. Bolt-on Differential Privacy for Scalable Stochastic Gradient Descent-based Analytics. In Proceedings of the 2017 ACM International Conference on Management of Data (SIGMOD ’17) . ACM, Ne...

    2017

  45. [55]

    Danfeng Zhang and Daniel Kifer. 2017. LightDP: Towards automating differential privacy proofs. In POPL, Vol. 52. ACM, 888–901

    2017

  46. [56]

    Pierce, and Aaron Roth

    Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. Pierce, and Aaron Roth. 2019. Fuzzi: A Three-Level Logic for Differential Privacy. Accepted for publication in PACMPL / ICFP 2019. A ADDITIONAL CASE STUDIES A.1 Hyperparameter Tuning Each of the gradient descent algorithm...

    2019

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.