Conferences:

2022
On Incorrectness Logic and Kleene Algebra With Top and Tests - arxiv - with C. Zhang, A. Azevedo de Amorim, POPL 2022.
2022
A Separation Logic for Negative Dependence - with J. Bao, J. Hsu, J. Tassarotti, POPL 2022.
2022
The Complexity of Verifying Boolean Programs asDifferentially Private - with M. Bun, L. Glinskih, CSF 2022.
2021
Covariance-Aware Private Mean Estimation Without Private Covariance Estimation - arxiv - with G. Brown, A. Smith, J. Ullman, L. Zakynthinou, NeurIPS 2021, spotlight presentation.
2021
Multiclass versus Binary Differentially Private PAC Learning - arxiv - with M. Bun, S. Sivakumar, NeurIPS 2021.
2021
Higher-order probabilistic adversarial computations: categorical semantics and program logics - arxiv - with A. Aguirre, G. Barthe, D. Garg, S. Katsumata, T. Sato, ICFP 2021.
2021
A unifying type-theory for higher-order (amortized) cost analysis. - pdf@acm - with V. Rajani, D. Garg, J. Hoffmann, POPL 2021.
2021
Estimating Smooth GLM in Non-interactive Local Differential Privacy Model with Public Unlabeled Data. - pdf - with D. Wang, H. Zhang, J. Xu , ALT 2021.
2021
Coupled Relational Symbolic Execution for Differential Privacy - arxiv - with G.P. Farina, and S. Chong, ESOP 2021.
2021
Graded Hoare Logic and its Categorical Semantics - arxiv - with with S. Katsumata, D. Orchard, T. Sato , ESOP 2021.
2020
Probabilistic Programming Languages for Modeling Autonomous Systems. - with S. M. Shasmi, G. P. Farina, N. Napp, MFI 2020.
2020
The Complexity of Verifying Loop-Free Programs as Differentially Private. - arxiv - with K. Nissim, D. Purser, ICALP 2020.
2020
A Programming Framework for Differential Privacy with Accuracy Concentration Bounds - arxiv - with E. Lobo-Vesga, A. Russo, IEEE Security and Privacy 2020.
2020
Hypothesis Testing Interpretations and Renyi Differential Privacy - arxiv - with B. Balle, G. Barthe, J. Hsu, T. Sato, AISTATS 2020.
2019
Facility Location Problem in Differential Privacy Model Revisited - arxiv - with Y. Esencayi, S. Li, D. Wang, NeurIPS 2019.
2019
Privacy Amplification by Mixing and Diffusion Mechanisms - arxiv - with B. Balle, G. Barthe, J. Geumlek, NeurIPS 2019.
2019
Relational Symbolic Execution - arxiv - with G.P. Farina, and S. Chong, PPDP 2019.
2019
Relational Cost Analysis for Functional-Imperative Programs - arxiv - with W. Qu, and D. Garg, ICFP 2019.
2019
Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy - arxiv - with T. Sato, G. Barthe, J. Hsu, S. Katsumata, LICS 2019.
2019
Probabilistic Relational Reasoning via Metrics - arxiv - with A. Azevedo de Amorim, J. Hsu, S. Katsumata, LICS 2019.
2019
Bidirectional Type Checking for Relational Properties - arxiv - with E. Cicek, W. Qu, G. Barthe, D. Garg, PLDI 2019.
2019
Formal verification of higher-order probabilistic programs - arxiv - with T. Sato, A. Aguirre, G. Barthe, D. Garg, J. Hsu, POPL 2019.
2019
Locally Private Mean Estimation: Z-test and Tight Confidence Intervals - arxiv - with R. Rogers, O. Sheffet, AISTATS 2019.
2018
Efficient Empirical Risk Minimization with Smooth Loss Functions in Non-interactive Local Differential Privacy - arxiv - with D. Wang, J. Xu, NeurIPS 2018.
2018
Privacy Amplification by Subsampling: Tight Analyses via Couplings and Divergences - arxiv - with B. Balle, G. Barthe, NeurIPS 2018.
2018
Local Private Hypothesis Testing: Chi-Square Tests - pdf - with R. Rogers, ICML 2018.
2018
A Program Logic for Probabilistic Programs - pdf - with G. Barthe, T. Espitau, D. Gregoire, J. Hsu, P.-Y. Strub, ESOP 2018.
2018
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus - pdf - with A. Aguirre, G. Barthe, L. Birkedal, A. Bizjak, D. Garg, ESOP 2018.
2018
Monadic refinements for relational cost analysis - pdf - with I. Radicek, G. Barthe, D. Garg, F. Zuleger, POPL 2018, © ACM 2018.
2017
A Relational Logic for Higher-Order Programs - arxiv - with A. Aguirre, G. Barthe, D. Garg, P.-Y. Strub, ICFP 2017, © ACM 2017.
2017
Relational Cost Analysis - pdf - with E. Cicek, G. Barthe, D. Garg, J. Hoffmann, POPL 2017, © ACM 2017.
2017
A semantic account of metric preservation - pdf - with A. Azevedo de Amorim, J. Hsu, S. Katsumata, I. Cherigui, POPL 2017, © ACM 2017.
2016
Computer-aided verification in mechanism design - arxiv - with G. Barthe,E. J. Gallego Arias, J. Hsu, A. Roth, P.-Y. Strub, WINE 2016.
2016
Differentially Private Bayesian Programming- arxiv - with G. Barthe, G. P. Farina, E. J. Gallego Arias, A. D. Gordon, J. Hsu, P.-Y. Strub, CCS 2016, © ACM 2016.
2016
Advanced Probabilistic Couplings for Differential Privacy - arxiv - with G. Barthe, N. Fong, B. Grégoire, J. Hsu, and P.-Y. Strub, CCS 2016, © ACM 2016.
2016
Differentially Private Chi-Squared Hypothesis Testing: Goodness of Fit and Independence Testing - arxiv - with Hyun woo Lim, R. Rogers, S. Vadhan, ICML 2016.
2016
Combining Effects and Coeffects via Grading - pdf - with S. Katsumata, D. Orchard, T. Uustalu, F. Breuvart, ICFP 2016, © ACM 2016.
2016
A program logic for union bounds - arxiv - with G. Barthe, B. Grégoire, J. Hsu, and P.-Y. Strub, ICALP 2016.
2016
Sensitivity of Counting Queries - pdf - with M. Arapinis and D. Figueira, ICALP 2016.
2016
Proving differential privacy via probabilistic couplings - arxiv - with G. Barthe, B. Grégoire, J. Hsu, and P.-Y. Strub, LICS 2016.
2015
Algebras and Coalgebras in the Light Affine Lambda Calculus with R. Pechoux - HAL ICFP 2015, 2015.
2015
A Theory AB Toolbox - pdf - with J. Hsu, SNAPL, pp. 129-139, LIPIcs, 2015.
2015
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy - arxiv - with G. Barthe, E. J. Gallego Arias, J. Hsu, A. Roth, P.-Y. Strub POPL 2015, pp. 55-68 © ACM 2015.
2014
Dual Query: Practical Private Query Release for High Dimensional Data - arxiv - with E. J. Gallego Arias, J. Hsu, A. Roth, Z. S. Wu ICML 2014.
2014
Differential Privacy: An Economic Method for Choosing Epsilon - pdf - with J. Hsu, A. Haeberlen, S. Khanna, A. Narayan, B. C. Pierce, A. Roth CSF 2014 - © IEEE Computer Society 2014.
2014
Proving Differential Privacy in Hoare Logic - pdf - with G. Barthe, E. J. Gallego Arias, J. Hsu, C. Kunz, P.-Y. Strub CSF 2014 - © IEEE Computer Society 2014.
2014
A Core Quantitative Coeffect Calculus - pdf - with A. Brunel, D. Mazza, S. Zdancewic ESOP 2014, LNCS - © Springer-Verlag Berlin Heidelberg 2014.
2013
Linear Dependent Types for Differential Privacy - pdf - with A. Haeberlen, J. Hsu, A. Narayan and B. C. Pierce POPL 2013, pp. 357-370 © ACM 2013.
2011
Linearity and PCF: a semantic insight! - pdf - with Luca Paolini and Mauro Piccolo ICFP 2011, pp 372-384 © ACM 2011.
2011
Linear dependent types and relative completeness - pdf - with Ugo Dal Lago LICS 2011, pp 133-142 © IEEE Computer Society 2011.
2010
A polytime functional language from Light linear logic - pdf - with Patrick Baillot and Virgile Mogbil ESOP 2010, LNCS, Volume 6012, pp 104-124 - © Springer-Verlag Berlin Heidelberg 2010.
2009
A by-level analysis of Multiplicative Exponential Linear Logic - pdf - with Luca Roversi and Luca Vercelli MFCS 2009, LNCS, Volume 5734, pp 344-355 - © Springer-Verlag Berlin Heidelberg 2009.
2009
Upper Bounds on Stream I/O Using Semantic Interpretations - pdf - with Romain Pechoux CSL 2009, LNCS, Volume 5771, pp 271-286 - © Springer-Verlag Berlin Heidelberg 2009.
2008
A Logical Account of PSPACE - pdf - with Jean-Yves Marion and Simona Ronchi Della Rocca POPL 2008, pp 121-131 - © ACM Sigplan - Sigact.
2007
A Soft Type assignment system for lambda-calculus - pdf - with Simona Ronchi Della Rocca CSL 2007, LNCS, Volume 4646, pp 253-267 - © Springer-Verlag Berlin Heidelberg 2007.

Journals:

2021
A Programming Language for Data Privacy with Accuracy Estimations - with E. Lobo-Vesga, A. Russo, ACM Transactions on Programming Languages and Systems, 2021.
2020
Empirical Risk Minimization in the Non-interactive Local Model of Differential Privacy. - pdf - with D. Wang, A. Smith, J. Xu. Journal of Machine Learning Research 21 (2020) 1-396.
2020
Privacy Profiles and Amplification by Subsampling - pdf - with B. Balle, G. Barthe. Journal of Privacy and Condidentiality, Volume 10, Number 1, 2020.
2019
A Relational Logic for Higher-Order Programs - pdf - with A. Aguirre, G. Barthe, D. Garg, P-Y. Strub. Journal of Functional Programming. Cambridge University Press. Vol 29, Special issue ICFP 2017. e16, 2019.
2018
Bridging the Gap between Computer Science and Legal Approaches to Privacy - pdf - with K. Nissim, A. Bembenek, A. Wood, M. Bun, U. Gasser, D. O'Brien, T. Steinke, S. Vadhan. Harvard Journal of Law \& Technology, Volume 31, Number 2 Spring 2018.
2018
Differential privacy: A primer for a non-technical audience - pdf - with A. Wood, M. Altman, A. Bembenek, M. Bun, J. Honaker, K. Nissim, D. R. O'Brien, T. Steinke, S. Vadhan. Vanderbilt Journal of Entertainment & Technology Law 21, no. 1 (2018): 209-275.
2016
Dual Query: Practical Private Query Release for High Dimensional Data - pdf - with E. J. Gallego Arias, J. Hsu, A. Roth, Z. S. Wu. Journal of Privacy and Confidentiality, Volume 7, Number 2, 53---77.
2016
Programming language techniques for differential privacy- pdf - with G. Barthe, J. Hsu, B. C. Pierce. Siglog News 3(1).
2015
On Bounding Space Usage of Streams Using Interpretation Analysis - HAL with Romain Pechoux - Science of Computer Programming.
2014
On the Reification of Semantic Linearity - pdf - with Luca Paolini and Mauro Piccolo. Mathematical Structure in Computer Science.
2014
Realizability Models for a Linear Dependent PCF - pdf - with A. Brunel. Theoretical Computer Science.
2012
Linear dependent types and relative completeness - pdf - with Ugo Dal Lago. Logical Methods in Computer Science. Volume 8(4) 12.
2012
An implicit characterization of PSPACE - pdf - with Jean-Yves Marion and Simona Ronchi Della Rocca. ACM Transactions on Computational Logic. Volume 13(2) 18.
2012
What is a model for a semantically Linear lambda-calculus? - pdf - with Mauro Piccolo. Journal of Logic and Computation - doi: 10.1093/logcom/exs023.
2009
From Light Logics to Type Assignments: a case study - pdf - with Simona Ronchi della Rocca. Logic Journal of the IGPL, Volume 17, pp 499-530.

Workshops:

2015
Really Natural Linear Indexed Type Checking - arxiv - with A. Azevedo de Amorim, E. J. Gallego Arias, J. Hsu IFL 2014 proceedings.
2013
Sensitivity Analysis using type-based constraints - pdf - with L. D'Antoni, E. J. Gallego Arias, A. Haeberlen, B. C. Pierce FPCDSL 2013 proceedings,  pp 43-50 - ACM.
2010
Global and local space properties of stream programs - pdf - with Romain Pechoux Fopara 2009, LNCS, Volume 6324 - © Springer-Verlag Berlin Heidelberg 2010.
2010
Categorical Models for a Semantically Linear lambda-calculus - pdf - with Mauro Piccolo Linearity 2009, EPTCS, Volume 22, pp 1-13.
2008
Type Inference for a polynomial Lambda-Calculus - pdf -with Simona Ronchi Della Rocca TYPES 2008, LNCS, Volume 5497, pp 136-152 - © Springer-Verlag Berlin Heidelberg 2009.
2008
Soft linear Logic and Polynomial Complexity Classes - pdf - with Jean-Yves Marion and Simona Ronchi Della Rocca LSFA 2007 post-proceedings, ENTCS, Volume 205, pp 67-87 - © 2008 Elsevier B.V.

Tutorials:

2014
Differential privacy: Language-based approaches - POPL 2014 - San Diego.

Online Books:

2014
Software Foundations - HTML - Benjamin C. Pierce, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, and Brent Yorgey

Thesis:

2007
Linearity: an Analytic Tool in the Study of Complexity and Semantics of Programming Languages - pdf - Phd Thesis, Università di Torino, Institut National Polytechnique de Lorraine.
2004
Inductive and Coinductive Techniques in the Operational Analysis of Functional Programs: an Introduction - pdf - Master Thesis, Università di Milano - Bicocca.
2002
Esecutore Simbolico per Java (in Italian) - pdf - Laurea Triennale Thesis, Universit&agraave; di Milano - Bicocca.

Notes:

2005
Induzione e Coinduzione - pdf - in Italian.
2005
Martin Lof's Type theory - pdf - Talk

DBLP

Contacts:

Boston University
Department of Computer Science
111 Cummington Mall, Room 116
Boston, MA 02215, USA

e-mail: gaboardi@bu.edu
phone: +1 671-353-3971