Travelled to:1 × China
1 × Cyprus
1 × France
1 × India
1 × Italy
1 × Japan
1 × Portugal
1 × Switzerland
2 × Canada
2 × USA
Collaborated with:J.Hsu G.Barthe R.Péchoux D.G.0001 S.R.D.Rocca E.J.G.Arias U.D.Lago A.A.d.Amorim E.Çiçek A.Roth P.Strub L.Paolini M.Piccolo P.Baillot V.Mogbil J.Marion A.A.0001 Gian Pietro Farina S.Chong A.Brunel D.Mazza S.Zdancewic Z.S.Wu A.Haeberlen A.Narayan B.C.Pierce S.Katsumata Ikram Cherigui J.H.0002 I.Radicek F.Zuleger Weihao Qu L.Birkedal A.Bizjak T.Espitau B.Grégoire T.Sato
Talks about:relat (7) type (6) linear (5) calculus (4) probabilist (3) program (3) semant (3) logic (3) differenti (2) approxim (2)
Person: Marco Gaboardi
DBLP: Gaboardi:Marco
Contributed to:
2015
2015
2014
2014
201420132011
20112010
200920082007201820172018
20192019
2019Wrote 20 papers:
- ICFP-2015-GaboardiP #algebra #λ-calculus
- Algebras and coalgebras in the light affine λ calculus (MG, RP), pp. 114–126.
- POPL-2015-BartheGAHRS #approximate #design #difference #higher-order #privacy #refinement #relational
- Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy (GB, MG, EJGA, JH, AR, PYS), pp. 55–68.
- ESOP-2014-BrunelGMZ #calculus
- A Core Quantitative Coeffect Calculus (AB, MG, DM, SZ), pp. 351–370.
- ICML-c2-2014-GaboardiAHRW #query
- Dual Query: Practical Private Query Release for High Dimensional Data (MG, EJGA, JH, AR, ZSW), pp. 1170–1178.
- IFL-2014-AmorimGAH #linear #type checking
- Really Natural Linear Indexed Type Checking (AAdA, MG, EJGA, JH), p. 5.
- POPL-2013-GaboardiHHNP #dependent type #difference #linear #privacy
- Linear dependent types for differential privacy (MG, AH, JH, AN, BCP), pp. 357–370.
- ICFP-2011-GaboardiPP #exclamation #semantics
- Linearity and PCF: a semantic insight! (MG, LP, MP), pp. 372–384.
- LICS-2011-LagoG #dependent type #linear
- Linear Dependent Types and Relative Completeness (UDL, MG), pp. 133–142.
- ESOP-2010-BaillotGM #functional #linear #logic
- A PolyTime Functional Language from Light Linear Logic (PB, MG, VM), pp. 104–124.
- CSL-2009-GaboardiP #bound #semantics #using
- Upper Bounds on Stream I/O Using Semantic Interpretations (MG, RP), pp. 271–286.
- POPL-2008-GaboardiMR #logic
- A logical account of pspace (MG, JYM, SRDR), pp. 121–131.
- CSL-2007-GaboardiR #calculus
- A Soft Type Assignment System for λ -Calculus (MG, SRDR), pp. 253–267.
- ESOP-2018-0001BBBG0 #markov #probability #reasoning #relational #λ-calculus
- Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus (AA0, GB, LB, AB, MG, DG0), pp. 214–241.
- ESOP-2018-BartheEGGHS #logic #probability #source code
- An Assertion-Based Program Logic for Probabilistic Programs (GB, TE, MG, BG, JH, PYS), pp. 117–144.
- POPL-2017-AmorimGHKC #metric #semantics
- A semantic account of metric preservation (AAdA, MG, JH, SyK, IC), pp. 545–556.
- POPL-2017-CicekBG0H #cost analysis #relational
- Relational cost analysis (EÇ, GB, MG, DG0, JH0), pp. 316–329.
- POPL-2018-RadicekBG0Z #cost analysis #monad #relational
- Monadic refinements for relational cost analysis (IR, GB, MG, DG0, FZ), p. 32.
- PLDI-2019-CicekQBG0 #bidirectional #relational #type checking
- Bidirectional type checking for relational properties (EÇ, WQ, GB, MG, DG0), pp. 533–547.
- POPL-2019-SatoABGGH #approximate #convergence #higher-order #optimisation #probability #reasoning #source code #verification
- Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization (TS, AA0, GB, MG, DG0, JH), p. 30.
- PPDP-2019-FarinaCG #execution #relational #symbolic computation
- Relational Symbolic Execution (GPF, SC, MG), p. 14.