Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus

Alejandro Aguirre, Gilles Barthe, Lars Birkedal +3

Locally Private Mean Estimation: Z-test and Tight Confidence Intervals

Marco Gaboardi, Ryan Rogers, Or Sheffet

Differentially Private Chi-Squared Hypothesis Testing: Goodness of Fit and Independence Testing

Marco Gaboardi, Hyun woo Lim, Ryan Rogers +1

Probabilistic Relational Reasoning via Metrics

Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu +1

Dual Query: Practical Private Query Release for High Dimensional Data

Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu +2

Relational Symbolic Execution

Gian Pietro Farina, Stephen Chong, Marco Gaboardi

The paper introduces RelSym, a symbolic execution engine that can analyze relational properties—relationships between two program runs or inputs—enabling verification and refutatio…

Empirical Risk Minimization in Non-interactive Local Differential Privacy: Efficiency and High Dimensional Case

Di Wang, Marco Gaboardi, Jinhui Xu

An Implicit Characterization of PSPACE

Marco Gaboardi, Jean-Yves Marion, Simona Ronchi Della Rocca

PSI (Ψ): a Private data Sharing Interface

Marco Gaboardi, James Honaker, Gary King +4

Advanced Probabilistic Couplings for Differential Privacy

Gilles Barthe, Noémie Fong, Marco Gaboardi +3

An Assertion-Based Program Logic for Probabilistic Programs

Gilles Barthe, Thomas Espitau, Marco Gaboardi +3

Linear Dependent Types for Domain Specific Program Analysis (Extended Abstract)

Marco Gaboardi

Really Natural Linear Indexed Type Checking

Arthur Azevedo de Amorim, Emilio Jesús Gallego Arias, Marco Gaboardi +1

Differential Privacy: An Economic Method for Choosing Epsilon

Justin Hsu, Marco Gaboardi, Andreas Haeberlen +4

Local Private Hypothesis Testing: Chi-Square Tests

Marco Gaboardi, Ryan Rogers

Differentially Private Bayesian Programming

Gilles Barthe, Gian Pietro Farina, Marco Gaboardi +4

Categorical Models for a Semantically Linear Lambda-calculus

Marco Gaboardi, Mauro Piccolo

Proving differential privacy in Hoare logic

Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias +3

Computer-aided verification in mechanism design

Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias +3

Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy

Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias +3

Linear Dependent Types and Relative Completeness

Ugo Dal Lago, Marco Gaboardi

Privacy Amplification by Subsampling: Tight Analyses via Couplings and Divergences

Borja Balle, Gilles Barthe, Marco Gaboardi