Conferences:

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:

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, to appear.
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