For the most up to date list of publications please refer to dblp.
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.
Differentially Private Chi-Squared Hypothesis Testing: Goodness of Fit and Independence Testing - arxiv - with Hyun woo Lim, R. Rogers, S. Vadhan, ICML 2016.
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.
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.