A Soft Type Assignment System for lambda -Calculus. - Marco Gaboardi; Simona Ronchi Della Rocca (CSL, 2007)

Soft Linear Logic and Polynomial Complexity Classes. - Marco Gaboardi; Jean-Yves Marion; Simona Ronchi Della Rocca (LSFA, 2007)

Linearity : an analytic tool in the study of complexity and semantics of programming languages. (Linéarité : un outil analytique pour l'étude de la complexité et de la sémantique des langages de programmation). - Marco Gaboardi (2007)

A logical account of pspace. - Marco Gaboardi; Jean-Yves Marion; Simona Ronchi Della Rocca (POPL, 2008)

Type Inference for a Polynomial Lambda Calculus. - Marco Gaboardi; Simona Ronchi Della Rocca (TYPES, 2008)

Upper Bounds on Stream I/O Using Semantic Interpretations. - Marco Gaboardi; Romain Péchoux (CSL, 2009)

Global and Local Space Properties of Stream Programs. - Marco Gaboardi; Romain Péchoux (FOPARA, 2009)

A By-Level Analysis of Multiplicative Exponential Linear Logic. - Marco Gaboardi; Luca Roversi; Luca Vercelli (MFCS, 2009)

Categorical Models for a Semantically Linear Lambda-calculus - Marco Gaboardi; Mauro Piccolo (LINEARITY, 2009)

From light logics to type assignments: a case study. - Marco Gaboardi; Simona Ronchi Della Rocca (Log. J. IGPL, 2009)

A PolyTime Functional Language from Light Linear Logic. - Patrick Baillot; Marco Gaboardi; Virgile Mogbil (ESOP, 2010)

Linearity and PCF: a semantic insight! - Marco Gaboardi; Luca Paolini; Mauro Piccolo (ICFP, 2011)

Linear Dependent Types and Relative Completeness - Ugo Dal Lago; Marco Gaboardi (Log. Methods Comput. Sci., 2011)

An Implicit Characterization of PSPACE. - Marco Gaboardi; Jean-Yves Marion; Simona Ronchi Della Rocca (ACM Trans. Comput. Log., 2012)

Sensitivity analysis using type-based constraints. - Loris D'Antoni; Marco Gaboardi; Emilio Jesús Gallego Arias; Andreas Haeberlen; Benjamin C. Pierce (FPCDSL@ICFP, 2013)

Linear dependent types for differential privacy. - Marco Gaboardi; Andreas Haeberlen; Justin Hsu; Arjun Narayan; Benjamin C. Pierce (POPL, 2013)

Linear Dependent Types for Domain Specific Program Analysis (Extended Abstract). - Marco Gaboardi (CoRR, 2013)

Proving Differential Privacy in Hoare Logic. - Gilles Barthe; Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu; César Kunz; Pierre-Yves Strub (CSF, 2014)

Differential Privacy: An Economic Method for Choosing Epsilon. - Justin Hsu; Marco Gaboardi; Andreas Haeberlen; Sanjeev Khanna; Arjun Narayan; Benjamin C. Pierce; Aaron Roth 001 (CSF, 2014)

A Core Quantitative Coeffect Calculus. - Aloïs Brunel; Marco Gaboardi; Damiano Mazza; Steve Zdancewic (ESOP, 2014)

Really Natural Linear Indexed Type Checking. - Arthur Azevedo de Amorim; Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu (IFL, 2014)

What is a model for a semantically linear λ-calculus? - Marco Gaboardi; Mauro Piccolo (J. Log. Comput., 2014)

Algebras and coalgebras in the light affine Lambda calculus. - Marco Gaboardi; Romain Péchoux (ICFP, 2015)

Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. - Gilles Barthe; Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu; Aaron Roth 001; Pierre-Yves Strub (POPL, 2015)

A Theory AB Toolbox. - Marco Gaboardi; Justin Hsu (SNAPL, 2015)

On bounding space usage of streams using interpretation analysis. - Marco Gaboardi; Romain Péchoux (Sci. Comput. Program., 2015)

Logic and Verification Methods in Security and Privacy (NII Shonan Meeting 2015-16). - Marco Gaboardi; Vivek Nigam; Tachio Terauchi (NII Shonan Meet. Rep., 2015)

Realizability models for a linear dependent PCF. - Aloïs Brunel; Marco Gaboardi (Theor. Comput. Sci., 2015)

Differentially Private Bayesian Programming. - Gilles Barthe; Gian Pietro Farina; Marco Gaboardi; Emilio Jesús Gallego Arias; Andy Gordon 001; Justin Hsu; Pierre-Yves Strub (CCS, 2016)

Advanced Probabilistic Couplings for Differential Privacy. - Gilles Barthe; Noémie Fong; Marco Gaboardi; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (CCS, 2016)

Sensitivity of Counting Queries. - Myrto Arapinis; Diego Figueira; Marco Gaboardi (ICALP, 2016)

A Program Logic for Union Bounds. - Gilles Barthe; Marco Gaboardi; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (ICALP, 2016)

Combining effects and coeffects via grading. - Marco Gaboardi; Shin-ya Katsumata; Dominic A. Orchard; Flavien Breuvart; Tarmo Uustalu (ICFP, 2016)

Differentially Private Chi-Squared Hypothesis Testing: Goodness of Fit and Independence Testing. - Marco Gaboardi; Hyun-Woo Lim; Ryan M. Rogers; Salil P. Vadhan (ICML, 2016)

Proving Differential Privacy via Probabilistic Couplings. - Gilles Barthe; Marco Gaboardi; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (LICS, 2016)

Computer-Aided Verification for Mechanism Design. - Gilles Barthe; Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu; Aaron Roth 001; Pierre-Yves Strub (WINE, 2016)

Advanced Probabilistic Couplings for Differential Privacy. - Gilles Barthe; Marco Gaboardi; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (CoRR, 2016)

PSI (Ψ): a Private data Sharing Interface. - Marco Gaboardi; James Honaker; Gary King; Kobbi Nissim; Jonathan R. Ullman; Salil P. Vadhan (CoRR, 2016)

Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131). - Marco Gaboardi; Suresh Jagannathan; Ranjit Jhala; Stephanie Weirich (Dagstuhl Reports, 2016)

Dual Query: Practical Private Query Release for High Dimensional Data. - Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu; Aaron Roth 001; Zhiwei Steven Wu (J. Priv. Confidentiality, 2016)

Special Issue on the Theory and Practice of Differential Privacy. - Marco Gaboardi; Chris J. Skinner (J. Priv. Confidentiality, 2016)

On the reification of semantic linearity. - Marco Gaboardi; Luca Paolini; Mauro Piccolo (Math. Struct. Comput. Sci., 2016)

Programming language techniques for differential privacy. - Gilles Barthe; Marco Gaboardi; Justin Hsu; Benjamin C. Pierce (ACM SIGLOG News, 2016)

PLAS 2017: ACM SIGSAC Workshop on Programming Languages and Analysis for Security. - Nataliia Bielova; Marco Gaboardi (CCS, 2017)

A semantic account of metric preservation. - Arthur Azevedo de Amorim; Marco Gaboardi; Justin Hsu; Shin-ya Katsumata; Ikram Cherigui (POPL, 2017)

Relational cost analysis. - Ezgi Çiçek; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Jan Hoffmann 002 (POPL, 2017)

Type Systems for the Relational Verification of Higher Order Programs (Invited Talk). - Marco Gaboardi (FSCD, 2017)

Reasoning about Divergences for Relaxations of Differential Privacy. - Tetsuya Sato 001; Gilles Barthe; Marco Gaboardi; Justin Hsu; Shin-ya Katsumata (CoRR, 2017)

Resource Bound Analysis (Dagstuhl Seminar 17291). - Marco Gaboardi; Jan Hoffmann 002; Reinhard Wilhelm; Florian Zuleger (Dagstuhl Reports, 2017)

A relational logic for higher-order programs. - Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Pierre-Yves Strub (Proc. ACM Program. Lang., 2017)

Semantics of Effects, Resources, and Applications (NII Shonan Meeting 2017-4). - Marco Gaboardi; Shin-ya Katsumata (NII Shonan Meet. Rep., 2017)

Formal Verification of Differential Privacy. - Marco Gaboardi (PLAS@CCS, 2018)

Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. - Alejandro Aguirre 001; Gilles Barthe; Lars Birkedal; Ales Bizjak; Marco Gaboardi; Deepak Garg 001 (ESOP, 2018)

An Assertion-Based Program Logic for Probabilistic Programs. - Gilles Barthe; Thomas Espitau; Marco Gaboardi; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (ESOP, 2018)

Local Private Hypothesis Testing: Chi-Square Tests. - Marco Gaboardi; Ryan Rogers 002 (ICML, 2018)

Privacy Amplification by Subsampling: Tight Analyses via Couplings and Divergences. - Borja Balle; Gilles Barthe; Marco Gaboardi (NeurIPS, 2018)

Empirical Risk Minimization in Non-interactive Local Differential Privacy Revisited. - Di Wang 015; Marco Gaboardi; Jinhui Xu 001 (NeurIPS, 2018)

Efficient Empirical Risk Minimization with Smooth Loss Functions in Non-interactive Local Differential Privacy. - Di Wang 015; Marco Gaboardi; Jinhui Xu 001 (CoRR, 2018)

Metric Semantics for Probabilistic Relational Reasoning. - Arthur Azevedo de Amorim; Marco Gaboardi; Justin Hsu; Shin-ya Katsumata (CoRR, 2018)

Formal verification of higher-order probabilistic programs. - Tetsuya Sato 001; Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Justin Hsu (CoRR, 2018)

Special issue - Developments in implicit computational complexity, 2014 and 2015. - Marco Gaboardi; Ulrich Schöpp (Inf. Comput., 2018)

Monadic refinements for relational cost analysis. - Ivan Radicek; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Florian Zuleger (Proc. ACM Program. Lang., 2018)

Locally Private Mean Estimation: $Z$-test and Tight Confidence Intervals. - Marco Gaboardi; Ryan Rogers 002; Or Sheffet (AISTATS, 2019)

Probabilistic Relational Reasoning via Metrics. - Arthur Azevedo de Amorim; Marco Gaboardi; Justin Hsu; Shin-ya Katsumata (LICS, 2019)

Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy. - Tetsuya Sato 001; Gilles Barthe; Marco Gaboardi; Justin Hsu; Shin-ya Katsumata (LICS, 2019)

Privacy Amplification by Mixing and Diffusion Mechanisms. - Borja Balle; Gilles Barthe; Marco Gaboardi; Joseph Geumlek (NeurIPS, 2019)

Facility Location Problem in Differential Privacy Model Revisited. - Yunus Esencayi; Marco Gaboardi; Shi Li 001; Di Wang 015 (NeurIPS, 2019)

Bidirectional type checking for relational properties. - Ezgi Çiçek; Weihao Qu; Gilles Barthe; Marco Gaboardi; Deepak Garg 001 (PLDI, 2019)

Relational Symbolic Execution. - Gian Pietro Farina; Stephen Chong; Marco Gaboardi (PPDP, 2019)

Estimating Smooth GLM in Non-interactive Local Differential Privacy Model with Public Unlabeled Data. - Di Wang 015; Huanyu Zhang; Marco Gaboardi; Jinhui Xu 001 (CoRR, 2019)

The Complexity of Verifying Circuits as Differentially Private. - Marco Gaboardi; Kobbi Nissim; David Purser (CoRR, 2019)

Program for TPDP 2016. - Gilles Barthe; Christos Dimitrakakis; Marco Gaboardi; Andreas Haeberlen; Aaron Roth 001; Aleksandra B. Slavkovic (J. Priv. Confidentiality, 2019)

Special Issue on the Theory and Practice of Differential Privacy 2016. - Marco Gaboardi (J. Priv. Confidentiality, 2019)

Relational cost analysis for functional-imperative programs. - Weihao Qu; Marco Gaboardi; Deepak Garg 001 (Proc. ACM Program. Lang., 2019)

Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization. - Tetsuya Sato 001; Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Justin Hsu (Proc. ACM Program. Lang., 2019)

Hypothesis Testing Interpretations and Renyi Differential Privacy. - Borja Balle; Gilles Barthe; Marco Gaboardi; Justin Hsu; Tetsuya Sato 001 (AISTATS, 2020)

The Complexity of Verifying Loop-Free Programs as Differentially Private. - Marco Gaboardi; Kobbi Nissim; David Purser (ICALP, 2020)

Probabilistic Programming Languages for Modeling Autonomous Systems. - Seyed Mahdi Shamsi; Gian Pietro Farina; Marco Gaboardi; Nils Napp (MFI, 2020)

A Programming Framework for Differential Privacy with Accuracy Concentration Bounds. - Elisabet Lobo Vesga; Alejandro Russo; Marco Gaboardi (SP, 2020)

Controlling Privacy Loss in Survey Sampling (Working Paper). - Mark Bun; Jörg Drechsler; Marco Gaboardi; Audra McMillan (CoRR, 2020)

Empirical Risk Minimization in the Non-interactive Local Model of Differential Privacy. - Di Wang 015; Marco Gaboardi; Adam D. Smith 001; Jinhui Xu 001 (J. Mach. Learn. Res., 2020)

Privacy Profiles and Amplification by Subsampling. - Borja Balle; Gilles Barthe; Marco Gaboardi (J. Priv. Confidentiality, 2020)

Estimating Smooth GLM in Non-interactive Local Differential Privacy Model with Public Unlabeled Data. - Di Wang 015; Huangyu Zhang; Marco Gaboardi; Jinhui Xu 001 (ALT, 2021)

Coupled Relational Symbolic Execution for Differential Privacy. - Gian Pietro Farina; Stephen Chong; Marco Gaboardi (ESOP, 2021)

Graded Hoare Logic and its Categorical Semantics. - Marco Gaboardi; Shin-ya Katsumata; Dominic Orchard; Tetsuya Sato 001 (ESOP, 2021)

Covariance-Aware Private Mean Estimation Without Private Covariance Estimation. - Gavin Brown 003; Marco Gaboardi; Adam D. Smith 001; Jonathan R. Ullman; Lydia Zakynthinou (NeurIPS, 2021)

Multiclass versus Binary Differentially Private PAC Learning. - Satchit Sivakumar; Mark Bun; Marco Gaboardi (NeurIPS, 2021)

Programming Languages Techniques for Controlling Generalization Errors in Adaptive Data Analysis. - Marco Gaboardi (PPDP, 2021)

Relational cost analysis in a functional-imperative setting. - Weihao Qu; Marco Gaboardi; Deepak Garg 001 (J. Funct. Program., 2021)

Higher-order probabilistic adversarial computations: categorical semantics and program logics. - Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Shin-ya Katsumata; Tetsuya Sato 001 (Proc. ACM Program. Lang., 2021)

A unifying type-theory for higher-order (amortized) cost analysis. - Vineet Rajani; Marco Gaboardi; Deepak Garg 001; Jan Hoffmann 002 (Proc. ACM Program. Lang., 2021)

A Programming Language for Data Privacy with Accuracy Estimations. - Elisabet Lobo Vesga; Alejandro Russo; Marco Gaboardi (ACM Trans. Program. Lang. Syst., 2021)

On Facility Location Problem in the Local Differential Privacy Model. - Vincent Cohen-Addad; Yunus Esencayi; Chenglin Fan; Marco Gaboardi; Shi Li 001; Di Wang 015 (AISTATS, 2022)

The Complexity of Verifying Boolean Programs as Differentially Private. - Mark Bun; Marco Gaboardi; Ludmila Glinskih (CSF, 2022)

Controlling Privacy Loss in Sampling Schemes: An Analysis of Stratified and Cluster Sampling. - Mark Bun; Jörg Drechsler; Marco Gaboardi; Audra McMillan; Jayshree Sarathy (FORC, 2022)

Formalizing Algorithmic Bounds in the Query Model in EasyCrypt. - Alley Stoughton; Carol Chen; Marco Gaboardi; Weihao Qu (ITP, 2022)

A separation logic for negative dependence. - Jialu Bao; Marco Gaboardi; Justin Hsu; Joseph Tassarotti (Proc. ACM Program. Lang., 2022)

On incorrectness logic and Kleene algebra with top and tests. - Cheng Zhang 026; Arthur Azevedo de Amorim; Marco Gaboardi (Proc. ACM Program. Lang., 2022)

Bunched Fuzz: Sensitivity for Vector Metrics. - june wunder; Arthur Azevedo de Amorim; Patrick Baillot; Marco Gaboardi (ESOP, 2023)

SymRustC: A Hybrid Fuzzer for Rust. - Frédéric Tuong; Mohammad Omidvar Tehrani; Marco Gaboardi; Steven Y. Ko (ISSTA, 2023)

Stability Is Stable: Connections between Replicability, Privacy, and Adaptive Generalization. - Mark Bun; Marco Gaboardi; Max Hopkins; Russell Impagliazzo; Rex Lei; Toniann Pitassi; Satchit Sivakumar; Jessica Sorrell (STOC, 2023)

Differentially Private Confidence Intervals for Proportions under Stratified Random Sampling. - Shurong Lin; Mark Bun; Marco Gaboardi; Eric D. Kolaczyk; Adam Smith 006 (CoRR, 2023)

A Formal Model for Secure Multiparty Computation. - Amy Rathore; Marina Blanton; Marco Gaboardi; Lukasz Ziarek (CoRR, 2023)

Continual Release of Differentially Private Synthetic Data. - Mark Bun; Marco Gaboardi; Marcel Neunhoeffer; Wanrong Zhang 001 (CoRR, 2023)

Generalized Linear Models in Non-interactive Local Differential Privacy with Public Data. - Di Wang 015; Lijie Hu; Huanyu Zhang; Marco Gaboardi; Jinhui Xu 001 (J. Mach. Learn. Res., 2023)

Report on Logic in Computer Science (LICS'23). - Marco Gaboardi; Igor Walukiewicz (ACM SIGLOG News, 2023)

Domain Reasoning in TopKAT. - Cheng Zhang 026; Arthur Azevedo de Amorim; Marco Gaboardi (ICALP, 2024)

Programming Frameworks for Differential Privacy. - Marco Gaboardi; Michael Hay; Salil P. Vadhan (CoRR, 2024)

Continual Release of Differentially Private Synthetic Data from Longitudinal Data Collections. - Mark Bun; Marco Gaboardi; Marcel Neunhoeffer; Wanrong Zhang 001 (Proc. ACM Manag. Data, 2024)

Program Analysis for Adaptive Data Analysis. - Jiawen Liu; Weihao Qu; Marco Gaboardi; Deepak Garg 001; Jonathan R. Ullman (Proc. ACM Program. Lang., 2024)

Sensitivity by Parametricity. - Elisabet Lobo Vesga; Alejandro Russo; Marco Gaboardi; Carlos Tomé Cortiñas (Proc. ACM Program. Lang., 2024)

Session Types for the Concurrent Composition of Interactive Differential Privacy. - Victor Sannier; Patrick Baillot; Marco Gaboardi (CSF, 2025)

A Kleene Algebra with Tests for Union Bound Reasoning About Probabilistic Programs. - Leandro Gomes 001; Patrick Baillot; Marco Gaboardi (CSL, 2025)

Kleene Algebra with Commutativity Conditions Is Undecidable. - Arthur Azevedo de Amorim; Cheng Zhang 026; Marco Gaboardi (CSL, 2025)

BiGKAT: An Algebraic Framework for Relational Verification of Probabilistic Programs. - Leandro Gomes 001; Patrick Baillot; Marco Gaboardi (FoSSaCS, 2025)

Probabilistic Refinement Session Types. - Qiancheng Fu; Ankush Das; Marco Gaboardi (Proc. ACM Program. Lang., 2025)

Cryptis: Cryptographic Reasoning in Separation Logic. - Arthur Azevedo de Amorim; Amal Ahmed 001; Marco Gaboardi (CoRR, 2025)