%%%%%%%%%%%%%%%%%%%%%%%%%%%% UNPUBLISHED %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @unpublished{BEGHS16, title = {Relational expectation properties by probabilistic coupling}, author = {Barthe, Gilles and Espitau, Thomas and Gr{\'e}goire, Benjamin and Hsu, Justin and Strub, {P}ierre-{Y}ves}, year = 2016, jh = yes, url = {http://justinh.su/files/papers/bounded.pdf}, } @unpublished{BEGGHS16, title = {Formal certification of randomized algorithms}, author = {Barthe, Gilles and Espitau, Thomas and Gaboardi, Marco and Gr{\'e}goire, Benjamin and Hsu, Justin and Strub, {P}ierre-{Y}ves}, year = 2016, jh = yes, url = {http://justinh.su/files/papers/ellora.pdf}, } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% JOURNALS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @article{GGHRW14, author = {Gaboardi, Marco and Gallego Arias, Emilio Jes{\'u}s and Hsu, Justin and Roth, Aaron and Wu, Zhiwei Steven}, title = {Dual Query: Practical private query release for high dimensional data}, journal = jpc, year = {2017}, month = {}, volume = {7}, number = {2}, pages = {53--77}, url = {http://arxiv.org/abs/1402.1526}, publisher = bepress, jh = yes, reviewed = yes, poster = {http://justinh.su/files/posters/dualquery.pdf}, note = "Previously published in " # icml14 # ", 2014." } @article{HHRRW14, author = {Hsu, Justin and Huang, Zhiyi and Roth, Aaron and Roughgarden, Tim and Wu, Zhiwei Steven}, title = {Private matchings and allocations}, journal = siamjc, year = {2016}, month = {}, volume = {45}, number = {6}, pages = {1953--1984}, doi = {10.1137/15100271X}, url = {http://arxiv.org/abs/1311.2828}, jh = yes, reviewed = yes, poster = {http://justinh.su/files/posters/matchings.pdf}, note = "Previously published in " # stoc14 # ", 2014." } %%%%%%%%%%%%%%%%%%%%%%%%%%%% CONFERENCES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @inproceedings{BEHSS17, title = {$\star$-Liftings for differential privacy}, author = {Barthe, Gilles and Espitau, Thomas and Hsu, Justin and Sato, Tetsuya and Strub, {P}ierre-{Y}ves}, booktitle = icalp17, year = 2017, url = {https://arxiv.org/abs/1705.00133}, jh = yes, plclub = yes, reviewed = yes, note = "To appear." } @inproceedings{BEGHS17, title = {Proving uniformity and independence by self-composition and coupling}, author = {Barthe, Gilles and Espitau, Thomas and Gr{\'e}goire, Benjamin and Hsu, Justin and Strub, {P}ierre-{Y}ves}, booktitle = lpar17, year = 2017, url = {https://arxiv.org/abs/1701.06477}, jh = yes, plclub = yes, reviewed = yes, } @inproceedings{BGHS16, title = {Coupling proofs are probabilistic product programs}, author = {Barthe, Gilles and Gr{\'e}goire, Benjamin and Hsu, Justin and Strub, {P}ierre-{Y}ves}, booktitle = popl17, year = 2017, url = {http://arxiv.org/abs/1607.03455}, slides = {http://justinh.su/files/slides/products.pdf}, jh = yes, plclub = yes, reviewed = yes, acceptance = {64/282=0.22}, } @inproceedings{ACGHK16, title = {A semantic account of metric preservation}, author = {de Amorim, Arthur Azevedo and Gaboardi, Marco and Hsu, Justin and Katsumata, {Shin-ya} and Cherigui, Ikram}, booktitle = popl17, year = 2017, url = {http://arxiv.org/abs/1702.00374}, jh = yes, plclub = yes, reviewed = yes, acceptance = {64/282=0.22}, } @inproceedings{HKM-verif16, title = {Computer-aided verification in mechanism design}, author = {Barthe, Gilles and Gaboardi, Marco and Gallego Arias, Emilio Jes{\'u}s and Hsu, Justin and Roth, Aaron and Strub, Pierre-Yves}, booktitle = wine16, year = 2016, url = {http://arxiv.org/abs/1502.04052}, slides = {http://justinh.su/files/slides/bic.pdf}, jh = yes, plclub = yes, reviewed = yes, } @inproceedings{BGGHS16c, title = {Advanced probabilistic couplings for differential privacy}, author = {Barthe, Gilles and Fong, No{\'e}mie and Gaboardi, Marco and Gr{\'e}goire, Benjamin and Hsu, Justin and Strub, {P}ierre-{Y}ves}, booktitle = ccs16, year = 2016, url = {https://arxiv.org/abs/1606.07143}, jh = yes, plclub = yes, reviewed = yes, acceptance = {137/831=0.17}, slides = {http://justinh.su/files/slides/advanced.pdf}, } @inproceedings{privinfer, title = {Differentially private {B}ayesian programming}, author = {Barthe, Gilles and Farina, Gian Pietro and Gaboardi, Marco and Gallego Arias, Emilio Jes{\'u}s and Gordon, Andy and Hsu, Justin and Strub, Pierre-Yves}, booktitle = ccs16, year = {2016}, url = {https://arxiv.org/abs/1605.00283}, jh = yes, plclub = yes, reviewed = yes, acceptance = {137/831=0.17}, } @inproceedings{BEFFH16, title = {Synthesizing probabilistic invariants via {D}oob's decomposition}, author = {Barthe, Gilles and Espitau, Thomas and Ferrer Fioriti, Luis Mar{\'i}a and Hsu, Justin}, booktitle = cav16, pages = {43--61}, volume = {9779}, series = lncs, year = 2016, publisher = springer, url = {https://arxiv.org/abs/1605.02765}, jh = yes, plclub = yes, reviewed = yes, acceptance = {46/195=0.24}, } @inproceedings{BGGHS16b, title = {A program logic for union bounds}, author = {Barthe, Gilles and Gaboardi, Marco and Gr{\'e}goire, Benjamin and Hsu, Justin and Strub, {P}ierre-{Y}ves}, booktitle = icalp16, pages = {107:1--107:15}, volume = {55}, series = lipics, year = 2016, publisher = dagstuhl, url = {http://arxiv.org/abs/1602.05681}, jh = yes, plclub = yes, reviewed = yes, acceptance = {146/515=0.28}, } @inproceedings{BGGHS16, title = {Proving differential privacy via probabilistic couplings}, author = {Barthe, Gilles and Gaboardi, Marco and Gr{\'e}goire, Benjamin and Hsu, Justin and Strub, {P}ierre-{Y}ves}, booktitle = lics16, pages = {749--758}, year = 2016, url = {http://arxiv.org/abs/1601.05047}, jh = yes, plclub = yes, reviewed = yes, slides = {http://justinh.su/files/slides/approx-couplings.pdf}, } @inproceedings{HMRRV16, title = {Do prices coordinate markets?}, author = {Hsu, Justin and Morgenstern, Jamie and Rogers, Ryan and Roth, Aaron and Vohra, Rakesh}, booktitle = stoc16, pages = {440--453}, year = 2016, url = {http://arxiv.org/abs/1511.00925}, jh = yes, reviewed = yes, acceptance = {92/370=0.25}, } @inproceedings{HHRW16, author = {Hsu, Justin and Huang, Zhiyi and Roth, Aaron and Wu, Zhiwei Steven}, title = {Jointly private convex programming}, booktitle = soda16, pages = {580--599}, year = {2016}, url = {http://arxiv.org/abs/1411.0998}, jh = yes, reviewed = yes, slides = {http://justinh.su/files/slides/privdude.pdf}, acceptance = {146/527=0.28}, } @inproceedings{BEGHSS15, title = {Relational reasoning via probabilistic coupling}, author = {Barthe, Gilles and Espitau, Thomas and Gr{\'e}goire, Benjamin and Hsu, Justin and Stefanesco, L{\'e}o and Strub, {P}ierre-{Y}ves}, booktitle = lpar15, pages = {387--401}, volume = {9450}, series = lncs, year = 2015, publisher = springer, url = {http://arxiv.org/abs/1509.03476}, jh = yes, plclub = yes, reviewed = yes, slides = {http://justinh.su/files/slides/couplings.pdf}, acceptance = {43/92=0.47}, } @inproceedings{AHJ15, title = {Online assignment with heterogeneous tasks in crowdsourcing markets}, author = {Assadi, Sepehr and Hsu, Justin and Jabbari, Shahin}, booktitle = hcomp15, pages = {12--21}, year = {2015}, url = {http://arxiv.org/abs/1508.03593}, jh = yes, reviewed = yes, } @inproceedings{GHaccuracy, author = {Marco Gaboardi and Justin Hsu}, title = {A {Theory AB} toolbox}, year = {2015}, booktitle = snapl15, pages = {129--139}, volume = {32}, series = lipics, publisher = dagstuhl, url = {http://justinh.su/files/papers/theory-ab.pdf}, jh = yes, plclub = yes, reviewed = yes, slides = {http://justinh.su/files/slides/theory-ab.pdf}, } @inproceedings{BGGHRS15, title = {Higher-order approximate relational refinement types for mechanism design and differential privacy}, author = {Barthe, Gilles and Gaboardi, Marco and Gallego Arias, Emilio Jes{\'u}s and Hsu, Justin and Roth, Aaron and Strub, Pierre-Yves}, booktitle = popl15, pages = {55--68}, year = {2015}, url = {http://arxiv.org/abs/1407.6845}, jh = yes, plclub = yes, reviewed = yes, slides = {http://justinh.su/files/slides/hoare2.pdf}, acceptance = {52/227=0.23}, } @inproceedings{AGGH14, author = {de Amorim, Arthur Azevedo and Gaboardi, Marco and Gallego Arias, Emilio Jes{\'u}s and Hsu, Justin}, title = {Really natural linear indexed type-checking}, booktitle = {Symposium on Implementation and Application of Functional Programming Languages (IFL), Boston, Massachusetts}, pages = {5:1--5:12}, year = {2014}, publisher = acmpress, url = {http://arxiv.org/abs/1503.04522}, jh = yes, plclub = yes, reviewed = yes, slides = {http://justinh.su/files/slides/dfuzz-tc.pdf}, } @inproceedings{BGGHKS14, author = {Barthe, Gilles and Gaboardi, Marco and Gallego Arias, Emilio Jes{\'u}s and Hsu, Justin and Kunz, C\'esar and Strub, Pierre-Yves}, title = {Proving differential privacy in {H}oare logic}, booktitle = csf14, pages = {411--424}, year = {2014}, url = {http://arxiv.org/abs/1407.2988}, jh = yes, plclub = yes, reviewed = yes, acceptance = {29/83=0.35}, } @inproceedings{HGH14, author = {Hsu, Justin and Gaboardi, Marco and Haeberlen, Andreas and Khanna, Sanjeev and Narayan, Arjun and Pierce, Benjamin C. and Roth, Aaron}, title = {Differential privacy: An economic method for choosing epsilon}, booktitle = csf14, pages = {398--410}, year = 2014, url = {http://arxiv.org/abs/1402.3329}, jh = yes, plclub = yes, reviewed = yes, slides = {http://justinh.su/files/slides/epsilon.pdf}, acceptance = {29/83=0.35}, } @inproceedings{HRRU14, author = {Hsu, Justin and Roth, Aaron and Roughgarden, Tim and Ullman, Jonathan}, title = {Privately solving linear programs}, booktitle = icalp14, pages = {612--624}, volume = 8572, series = lncs, year = {2014}, publisher = springer, url = {http://arxiv.org/abs/1402.3631}, jh = yes, reviewed = yes, slides = {http://justinh.su/files/slides/priv-lp.pdf}, acceptance = {136/477=0.29}, } inproceedings{GGHRW14, author = {Gaboardi, Marco and Gallego Arias, Emilio Jes{\'u}s and Hsu, Justin and Roth, Aaron and Wu, Zhiwei Steven}, title = {Dual Query: Practical private query release for high dimensional data}, booktitle = icml14, pages = {1170--1178}, volume = {32}, series = jmlrproc, year = {2014}, publisher = jmlr, reviewed = yes, url = {http://arxiv.org/abs/1402.1526}, jh = yes, slides = {http://justinh.su/files/slides/dualquery.pdf}, poster = {http://justinh.su/files/poser/dualquery.pdf}, acceptance = {310/1238=0.25}, } inproceedings{HHRRW14, author = {Hsu, Justin and Huang, Zhiyi and Roth, Aaron and Roughgarden, Tim and Wu, Zhiwei Steven}, title = {Private matchings and allocations}, booktitle = stoc14, year = {2014}, reviewed = yes, pages = {21--30}, url = {http://arxiv.org/abs/1311.2828}, timestamp = {Wed, 22 Oct 2014 14:44:14 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/stoc/HsuHRRW14}, bibsource = {dblp computer science bibliography, http://dblp.org}, jh = yes, poster = {http://justinh.su/files/poster/matchings.pdf}, acceptance = {91/319=0.29}, } @inproceedings{WHE13, title = {{S}ystem {FC} with explicit kind equality}, author = {Weirich, Stephanie and Hsu, Justin and Eisenberg, Richard A.}, booktitle = icfp13, pages = {275--286}, year = {2013}, url = {http://www.cis.upenn.edu/~justhsu/docs/nokinds.pdf}, jh = yes, plclub = yes, reviewed = yes, acceptance = {40/133=0.30}, } @inproceedings{HRU13, title = {Differential privacy for the analyst via private equilibrium computation}, author = {Hsu, Justin and Roth, Aaron and Ullman, Jonathan}, url = {http://arxiv.org/abs/1211.0877}, booktitle = stoc13, pages = {341--350}, year = {2013}, jh = yes, reviewed = yes, slides = {http://justinh.su/files/slides/analyst-priv.pdf}, acceptance = {100/360=0.28}, } @inproceedings{GHHNP13, title = {Linear dependent types for differential privacy}, author = {Gaboardi, Marco and Haeberlen, Andreas and Hsu, Justin and Narayan, Arjun and Pierce, Benjamin C.}, booktitle = popl13, pages = {357--370}, url = {http://dl.acm.org/citation.cfm?id=2429113}, year = {2013}, jh = yes, plclub = yes, reviewed = yes, acceptance = {51/220=0.23}, } @inproceedings{HKR12, title = {Distributed private heavy hitters}, author = {Hsu, Justin and Khanna, Sanjeev and Roth, Aaron}, booktitle = icalp12, pages = {461--472}, volume = {7391}, series = lncs, year = {2012}, publisher = springer, url = {http://arxiv.org/abs/1202.4910}, note = {Thanks to Raef Bassily and Adam Smith for spotting an error, now fixed.}, jh = yes, reviewed = yes, slides = {http://justinh.su/files/slides/heavy-hh.pdf}, acceptance = {123/433=0.28}, } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% SURVEYS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @article{Murawski:2016:2893582, title = {Programming language techniques for differential privacy}, author = {Barthe, Gilles and Gaboardi, Marco and Hsu, Justin and Pierce, Benjamin C.}, pages = {34--53}, journal = {ACM SIGLOG News}, month = jan, year = {2016}, volume = {3}, number = {1}, url = {http://siglog.hosting.acm.org/wp-content/uploads/2016/01/siglog_news_7.pdf}, jh = yes, plclub = yes, reviewed = no, } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% WORKSHOPS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @inproceedings{GGHHP13, title = {Automatic sensitivity analysis using linear dependent types}, author = {Gaboardi, Marco and Gallego Arias, Emilio Jes{\'u}s and Haeberlen, Andreas and Hsu, Justin and Pierce, Benjamin C.}, url = {http://fopara2013.cs.unibo.it/paper_8.pdf}, booktitle = fopara, year = {2013}, jh = yes, plclub = yes, reviewed = no, } @inproceedings{HsuTaxes, author = {Justin Hsu}, title = {Death, taxes, and formal verification (Abstract)}, year = {2015}, booktitle = snapl15, jh = yes, plclub = yes, reviewed = no, slides = {http://justinh.su/files/slides/taxes.pdf}, url = {http://justinh.su/files/papers/taxes.pdf} } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% TALKS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @talk{wine16-talk, title = {Computer-aided verification in mechanism design}, organization = wine16, year = 2016, month = dec, jh = yes, } @talk{cornell16-talk, title = {Approximate Probabilistic Coupling and Differential Privacy}, organization = {Theory Seminar, Cornell University}, year = 2016, month = oct, jh = yes, } @talk{ccs16-talk, title = {Advanced Probabilistic Couplings for Differential Privacy}, organization = ccs16, year = 2016, month = oct, jh = yes, } @talk{psu16-talk, title = {Differential Privacy as an Approximate Coupling}, organization = {Theory Seminar, Pennsylvania State University}, year = 2016, month = oct, jh = yes, } @talk{cmu16-talk, title = {Relational reasoning via probabilistic coupling}, organization = {Principles of Programming Seminar, Carnegie Mellon University}, year = 2016, month = oct, jh = yes, } @talk{jhu16-talk, title = {Approximate Probabilistic Coupling and Differential Privacy}, organization = {Theory Seminar, Johns Hopkins University}, year = 2016, month = oct, jh = yes, } @talk{msrc16-talk, title = {Formal Verification of Randomized Algorithms}, organization = {Constructive Security Seminar, MSR Cambridge UK}, year = 2016, month = jul, jh = yes, } @talk{lics16-talk, title = {Proving Differential Privacy via Probabilistic Couplings}, organization = lics16, year = 2016, month = jul, jh = yes, } @talk{tpdp16-talk, title = {Differential Privacy is an Approximate Probabilistic Coupling}, organization = {Workshop on the Theory and Practice of Differential Privacy (TPDP)}, year = 2016, month = jun, jh = yes, } @talk{crcs16-talk, title = {Differential Privacy is an Approximate Probabilistic Coupling}, organization = {CRCS Seminar, Harvard}, year = 2016, month = jun, jh = yes, } @talk{njpls16-talk, title = {A program logic for union bounds}, organization = {NJ Programming Languages and Systems Seminar (NJPLS)}, year = 2016, month = may, jh = yes, } @talk{uwisc16-talk, title = {Relational reasoning via probabilistic coupling}, organization = {PL Seminar, University of Wisconsin}, year = 2016, month = may, jh = yes, } @talk{soda16-talk, title = {Jointly Private Convex Programming}, organization = soda16, year = 2016, month = jan, jh = yes, } @talk{lpar15-talk, title = {Relational reasoning via probabilistic coupling}, organization = lpar15, year = 2015, month = nov, jh = yes, } @talk{nsf-sfm15-talk, title = {What are we measuring, anyways?}, organization = {NSF Workshop on Formal Methods for Information Security}, year = 2015, month = nov, jh = yes, } @talk{tau15-talk, title = {Language-based Verification for Differential Privacy}, organization = {Tel Aviv University}, year = 2015, month = nov, jh = yes, } @talk{shonan15-talk, title = {Language-based Verification for Differential Privacy}, organization = {Shonan Meeting on Logic and Verification Methods in Security and Privacy}, year = 2015, month = nov, jh = yes, } @talk{tohoku15-talk, title = {Relational reasoning via probabilistic coupling}, organization = {Tohoku University}, year = 2015, month = oct, jh = yes, } @talk{tit15-talk, title = {Jointly Private Convex Programming}, organization = {Tokyo Institute of Technology}, year = 2015, month = oct, jh = yes, } @talk{snapl15b-talk, title = {Death, Taxes, and Formal Verification}, organization = snapl15, year = 2015, month = may, jh = yes, } @talk{snapl15a-talk, title = {A {Theory AB} Toolbox}, organization = snapl15, year = 2015, month = may, jh = yes, } @talk{cornell15-talk, title = {Verifying Accuracy of Randomized Algorithms}, organization = {Cornell PL Discussion Group}, year = 2015, month = mar, jh = yes, } @talk{popl15-talk, title = {Higher-Order Relational Refinement Types for Mechanism Design and Differential Privacy}, organization = popl15, year = 2015, month = jan, jh = yes, } @talk{lix14-talk, title = {Jointly Private Convex Programming}, organization = {Com\`ete-Parsifal Seminar, {LIX}, \'Ecole Polytechnique}, year = 2014, month = nov, jh = yes, } @talk{dundee14-talk, title = {Jointly Private Convex Programming}, organization = {University of Dundee}, year = 2014, month = nov, jh = yes, } @talk{csf14-talk, title = {Differential Privacy: An Economic Method for Choosing Epsilon}, organization = csf14, year = 2014, month = jul, jh = yes, } @talk{icalp14-talk, title = {Privately Solving Linear Programs}, organization = icalp14, year = 2014, month = jul, jh = yes, } @talk{simons13-talk, title = {Dual Query Release}, organization = {Simons workshop on Big Data and Differential Privacy}, year = 2013, month = dec, jh = yes, } @talk{lix13-talk, title = {Private Matchings and Allocations}, organization = {Com\`ete-Parsifal Seminar, {LIX}, \'Ecole Polytechnique}, year = 2013, month = dec, jh = yes, } @talk{stoc13-talk, title = {Private Equilibrium Computation for Analyst Privacy}, organization = stoc13, year = 2013, month = jun, jh = yes, } @talk{dimacs12-talk, title = {Analyst Privacy---the State Strikes Back!}, organization = {{DIMACS} Workshop on Recent Work on Differential Privacy across Computer Science}, year = 2012, month = oct, jh = yes, } @talk{icalp12-talk, title = {Distributed Private Heavy Hitters}, organization = icalp12, year = 2012, month = jul, jh = yes, } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% OTHER %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @article{job-matching, title = {Job Matching, Coalition Formation, and Gross Substitutes}, volume = {50}, number = {6}, urldate = {2013--07--07}, journal = {Econometrica}, author = {Kelso, Alexander and Crawford, Vincent}, year = {1982}, pages = {1483--1504}, url = {http://EconPapers.repec.org/RePEc:ecm:emetrp:v:50:y:1982:i:6:p:1483-1504} } @article{CSS10, title = {Private and continual release of statistics}, volume = {14}, url = {http://eprint.iacr.org/2010/076.pdf}, number = {3}, urldate = {2013--06--23}, journal = tissec, author = {Chan, T.-H. Hubert and Shi, Elaine and Song, Dawn}, year = {2011}, pages = {26}, } @inproceedings{DNPR10, title = {Differential privacy under continual observation}, author = {Dwork, Cynthia and Naor, Moni and Pitassi, Toniann and Rothblum, Guy N.}, url = {http://www.mit.edu/~rothblum/papers/continalobs.pdf}, booktitle = stoc10, pages = {715--724}, year = {2010}, } @inproceedings{DNV12, title = {The privacy of the analyst and the power of the state}, author = {Dwork, Cynthia and Naor, Moni and Vadhan, Salil}, booktitle = focs12, pages = {400--409}, url = {http://projects.iq.harvard.edu/files/privacytools/files/06375318.pdf}, year = {2012} } @article{PR13, title = {Privacy and Mechanism Design}, author = {Pai, Mallesh and Roth, Aaron}, url = {http://arxiv.org/abs/1306.2083}, journal = sigecom, year = {2013} } @inproceedings{NRS07, title = {Smooth sensitivity and sampling in private data analysis}, url = {http://www.cse.psu.edu/~asmith/pubs/NRS07/NRS07-full-draft-v1.pdf}, author = {Nissim, Kobbi and Raskhodnikova, Sofya and Smith, Adam}, booktitle = stoc07, pages = {75--84}, year = {2007}, } @inproceedings{RR14, title = {Asymptotically truthful equilibrium selection in large congestion games}, author = {Rogers, Ryan and Roth, Aaron}, booktitle = ec14, pages = {771--782}, year = {2014}, url = {http://arxiv.org/abs/1311.2625} } @inproceedings{GLMRT10, title = {Differentially private combinatorial optimization}, url = {http://arxiv.org/abs/0903.4510}, author = {Gupta, Anupam and Ligett, Katrina and Mc{S}herry, Frank and Roth, Aaron and Talwar, Kunal}, booktitle = soda10, pages = {1106--1125}, year = {2010}, } @article{GS99, title = {Walrasian equilibrium with gross substitutes}, author = {Gul, Faruk and Stacchetti, Ennio}, url = {http://www.princeton.edu/~fgul/walras.pdf}, journal = jet, volume = {87}, number = {1}, pages = {95--124}, year = {1999}, publisher = elsevier } @article{BLR08, title = {A learning theory approach to noninteractive database privacy}, author = {Blum, Avrim and Ligett, Katrina and Roth, Aaron}, journal = jacm, url = {http://arxiv.org/abs/1109.2229}, volume = {60}, number = {2}, pages = {12}, year = {2013}, } @inproceedings{HR10, title = {A multiplicative weights mechanism for privacy-preserving data analysis}, author = {Hardt, Moritz and Rothblum, Guy N}, url = {http://www.mit.edu/~rothblum/papers/pmw.pdf}, booktitle = focs10, pages = {61--70}, year = {2010}, } @inproceedings{DN03, title = {Revealing information while preserving privacy}, author = {Dinur, Irit and Nissim, Kobbi}, url = {http://www.cse.psu.edu/~asmith/privacy598/papers/dn03.pdf}, booktitle = pods03, pages = {202--210}, year = {2003}, } @article{DR14, author = {Cynthia Dwork and Aaron Roth}, title = {The Algorithmic Foundations of Differential Privacy}, journal = {Foundations and Trends in Theoretical Computer Science}, year = {2014}, volume = {9}, number = {3--4}, pages = {211--407}, url = {http://dx.doi.org/10.1561/0400000042}, timestamp = {Tue, 28 Oct 2014 14:00:24 +0100}, biburl = {http://dblp.uni-trier.de/rec/bib/journals/fttcs/DworkR14}, bibsource = {dblp computer science bibliography, http://dblp.org} } @inproceedings{KPRU14, title = {Mechanism Design in Large Games: Incentives and Privacy}, url = {http://arxiv.org/abs/1207.4084}, author = {Kearns, Michael and Pai, Mallesh and Roth, Aaron and Ullman, Jonathan}, pages = {403--410}, booktitle = itcs14, year = {2014} } @inproceedings{DRV10, title = {Boosting and differential privacy}, url = {http://research.microsoft.com/pubs/155170/dworkrv10.pdf}, booktitle = focs10, author = {Dwork, Cynthia and Rothblum, Guy N. and Vadhan, Salil}, year = {2010}, keywords = {Algorithms, {CS}, {DP}, Learning Theory}, pages = {51--60}, } @inproceedings{FPT04, title = {The complexity of pure Nash equilibria}, author = {Fabrikant, Alex and Papadimitriou, Christos and Talwar, Kunal}, url = {http://research.microsoft.com/pubs/74349/pub10-pure.pdf}, booktitle = stoc04, pages = {604--612}, year = {2004}, } @article{MS96, title = {Potential games}, author = {Monderer, Dov and Shapley, Lloyd S.}, journal = geb, url = {http://www.cs.bu.edu/~steng/teaching/Fall2008/potential.pdf}, volume = {14}, number = {1}, pages = {124--143}, year = {1996}, publisher = {Elsevier} } @inproceedings{CK05, title = {The price of anarchy of finite congestion games}, author = {Christodoulou, George and Koutsoupias, Elias}, url = {http://dl.acm.org/citation.cfm?id=1060600}, booktitle = stoc05, pages = {67--73}, year = {2005}, } @inproceedings{AAE05, title = {The price of routing unsplittable flow}, author = {Awerbuch, Baruch and Azar, Yossi and Epstein, Amir}, booktitle = stoc05, url = {http://dl.acm.org/citation.cfm?id=1060599}, pages = {57--66}, year = {2005}, } @inproceedings{Rou09, title = {Intrinsic robustness of the price of anarchy}, author = {Roughgarden, Tim}, url = {http://theory.stanford.edu/~tim/papers/robust.pdf}, booktitle = stoc09, pages = {513--522}, year = {2009}, } @inproceedings{BHLR08, title = {Regret minimization and the price of total anarchy}, author = {Blum, Avrim and Haji{A}ghayi, Mohammad{T}aghi and Ligett, Katrina and Roth, Aaron}, url = {http://dl.acm.org/citation.cfm?id=1374430}, booktitle = stoc08, pages = {373--382}, year = {2008}, } @inproceedings{HLM12, title = {A Simple and Practical Algorithm for Differentially Private Data Release}, author = {Moritz Hardt and Katrina Ligett and Frank {McSherry}}, booktitle = nips12, pages = {2348--2356}, url = {http://arxiv.org/abs/1012.4763}, year = 2012 } @inproceedings{Ullman13, title = {Answering $n^{2+ o(1)}$ counting queries with differential privacy is hard}, author = {Ullman, Jonathan}, booktitle = stoc13, pages = {361--370}, url = {http://arxiv.org/abs/1207.6945}, year = 2013 } @inproceedings{MT07, author = {Frank McSherry and Kunal Talwar}, title = {Mechanism Design via Differential Privacy}, booktitle = focs07, pages = {94--103}, url = {http://doi.ieeecomputersociety.org/10.1109/FOCS.2007.41}, year = 2007 } @inproceedings{FS96, title = {Game theory, on-line prediction and boosting}, author = {Freund, Y. and Schapire, R.E.}, booktitle = colt96, pages = {325--332}, url = {http://dl.acm.org/citation.cfm?id=238163 }, year = 1996 } @inproceedings{BDMN05, title = {Practical privacy: the {SuLQ} framework}, author = {Avrim Blum and Cynthia Dwork and Frank Mc{S}herry and Kobbi Nissim}, booktitle = pods05, pages = {128--138}, url = {http://research.microsoft.com/pubs/64351/bdmn.pdf}, year = 2005 } @inproceedings{GRU12, title = {Iterative constructions and private data release}, author = {Gupta, Anupam and Roth, Aaron and Jonathan Ullman}, booktitle = tcc12, pages = {339--356}, url = {http://arxiv.org/abs/1107.3731}, year = 2012 } @inproceedings{airavat, author = {Indrajit Roy and Srinath Setty and Ann Kilzer and Vitaly Shmatikov and Emmett Witchel}, title = {Airavat: Security and Privacy for {MapReduce}}, booktitle = nsdi10, url = {http://dl.acm.org/citation.cfm?id=1855731 }, year = 2010 } @inproceedings{pinq, author = {{McSherry}, Frank}, booktitle = sigmod09, title = {Privacy integrated queries}, url = {http://research.microsoft.com/pubs/80218/sigmod115-mcsherry.pdf}, year = 2009 } @inproceedings{zhang-2011-privatemining, author = {Zhang, Ning and Li, Ming and Lou, Wenjing}, title = {Distributed Data Mining with Differential Privacy}, booktitle = icc11, url = {http://dl.acm.org/citation.cfm?id=1835868}, year = 2011 } @inproceedings{evfimievski-2002-associationrules, author = {Evfimievski, Alexandre and Srikant, Ramakrishnan and Agrawal, Rakesh and Gehrke, Johannes}, title = {Privacy preserving mining of association rules}, booktitle = kdd02, url = {http://www.cs.cornell.edu/johannes/papers/2002/kdd2002-privacy.pdf}, year = 2002 } @inproceedings{t-closeness, author = {Ninghui Li and Tiancheng Li and Suresh Venkatasubramanian}, title = {$t$-{C}loseness: {P}rivacy beyond $k$-anonymity and $l$-diversity}, booktitle = icde07, url = {https://www.cs.purdue.edu/homes/ninghui/papers/t_closeness_icde07.pdf}, year = 2007 } @article{k-anonymity, author = {Sweeney, Latanya}, title = {$k$-{A}nonymity: {A} model for protecting privacy}, journal = jufks, volume = {10}, number = {5}, year = {2002}, pages = {557--570}, url = {http://dl.acm.org/citation.cfm?id=774552} } @article{aol, author = {Michael Barbaro and Tom Zeller}, title = {A Face Is Exposed for {AOL} Searcher {N}o. 4417749}, journal = {The New York Times}, day = 9, month = aug, year = 2006, url = {http://www.nytimes.com/2006/08/09/technology/09aol.html} } @inproceedings{NV08, author = {Arvind Narayanan and Vitaly Shmatikov}, title = {Robust De-anonymization of Large Sparse Datasets}, booktitle = sp08, year = {2008}, pages = {111--125}, url = {http://arxiv.org/abs/cs/0610105} } @inproceedings{BLST10, author = {Raghav Bhaskar and Srivatsan Laxman and Adam Smith and Abhradeep Thakurta}, title = {Discovering frequent patterns in sensitive data}, booktitle = kdd10, pages = {503--512}, year = 2010, url = {http://dl.acm.org/citation.cfm?id=1835869} } @inproceedings{CM08, author = {Kamalika Chaudhuri and Claire Monteleoni}, title = {Privacy-preserving logistic regression}, booktitle = nips08, pages = {289--296}, year = 2008, url = {http://books.nips.cc/papers/files/nips21/NIPS2008_0964.pdf} } @article{CH11, title = {Sample Complexity Bounds for Differentially Private Learning}, author = {Chaudhuri, Kamalika and Hsu, Daniel}, journal = jmlr, volume = {19}, pages = {155--186}, url = {http://jmlr.org/proceedings/papers/v19/chaudhuri11a/chaudhuri11a.pdf}, year = {2011} } @article{BKOZ13-toplas, author = {Barthe, Gilles and K{\"{o}}pf, Boris and Olmedo, Federico and Zanella{-}B{\'{e}}guelin, Santiago}, title = {Probabilistic Relational Reasoning for Differential Privacy}, journal = toplas, volume = {35}, number = {3}, pages = {9}, year = {2013}, url = {http://software.imdea.org/~bkoepf/papers/toplas13.pdf}, } @inproceedings{ReedPierce10, author = {Jason Reed and Benjamin C. Pierce}, title = {Distance Makes the Types Grow Stronger: {A} Calculus for Differential Privacy}, booktitle = icfp10, year = 2010, url = {http://dl.acm.org/citation.cfm?id=1863568} } @inproceedings{winq, title = {A workflow for differentially-private graph synthesis}, author = {Proserpio, Davide and Goldberg, Sharon and {McSherry}, Frank}, booktitle = wosn12, year = 2012, pages = {13--18}, url = {http://arxiv.org/abs/1203.3453} } @article{KLNRS08, title = {What can we learn privately?}, author = {Kasiviswanathan, Shiva Prasad and Lee, Homin K. and Nissim, Kobbi and Raskhodnikova, Sofya and Smith, Adam}, journal = siamjc, volume = {40}, number = {3}, pages = {793--826}, year = {2011}, url = {http://arxiv.org/abs/0803.0924}, } @inproceedings{UV11, title = {{PCPs} and the hardness of generating private synthetic data}, author = {Ullman, Jonathan and Vadhan, Salil}, booktitle = tcc11, pages = {400--416}, url = {http://eccc.hpi-web.de/report/2010/017/revision/2/download}, year = {2011} } @inproceedings{DNRRV09, title = {On the complexity of differentially private data release: efficient algorithms and hardness results}, author = {Cynthia Dwork and Moni Naor and Omer Reingold and Guy N. Rothblum and Salil P. Vadhan}, booktitle = stoc09, pages = {381--390}, year = {2009}, url = {http://dl.acm.org/citation.cfm?id=1536467} } @article{AHK12, title = {The Multiplicative Weights Update Method: a Meta-Algorithm and Applications}, author = {Arora, Sanjeev and Hazan, Elad and Kale, Satyen}, journal = toc, volume = {8}, number = {1}, pages = {121--164}, url = {http://tocbeta.cs.uchicago.edu/articles/v008a006/v008a006.pdf}, year = {2012} } @phdthesis{Garg13, title = {Candidate Multilinear Maps}, author = {Sanjam Garg}, school = {{UCLA}}, year = {2013}, url = {http://www.cs.ucla.edu/~sanjamg/Sanjam%20Garg_files/sanjam-thesis.pdf} } @inproceedings{GargGentryHalevi13, title = {Candidate multilinear maps from ideal lattices}, author = {Garg, Sanjam and Gentry, Craig and Halevi, Shai}, booktitle = eucrypt13, pages = {1--17}, year = {2013}, url = {http://http://eprint.iacr.org/2012/610.pdf} } @article{BonehSilverberg03, title = {Applications of multilinear forms to cryptography}, author = {Boneh, Dan and Silverberg, Alice}, journal = {Contemporary Mathematics}, volume = {324}, number = {1}, pages = {71--90}, year = {2003}, publisher = {AMS}, url = {http://https://eprint.iacr.org/2002/080.pdf} } @inproceedings{barak2007privacy, title = {Privacy, accuracy, and consistency too: a holistic solution to contingency table release}, author = {Barak, Boaz and Chaudhuri, Kamalika and Dwork, Cynthia and Kale, Satyen and Mc{S}herry, Frank and Talwar, Kunal}, booktitle = pods07, pages = {273--282}, url = {http://research.microsoft.com/en-us/projects/DatabasePrivacy/contingency.pdf}, year = {2007} } @inproceedings{BNS13, title = {Characterizing the sample complexity of private learners}, author = {Beimel, Amos and Nissim, Kobbi and Stemmer, Uri}, booktitle = itcs13, pages = {97--110}, year = {2013}, url = {http://dl.acm.org/citation.cfm?id=2422450} } @article{CMS11, title = {Differentially private empirical risk minimization}, author = {Chaudhuri, Kamalika and Monteleoni, Claire and Sarwate, Anand D.}, journal = jmlr, volume = {12}, pages = {1069--1109}, year = {2011}, url = {http://jmlr.org/papers/volume12/chaudhuri11a/chaudhuri11a.pdf} } @article{RBHT09, title = {Learning in a Large Function Space: Privacy-Preserving Mechanisms for {SVM} Learning}, author = {Rubinstein, Benjamin I. P. and Bartlett, Peter L. and Huang, Ling and Taft, Nina}, journal = jpc, volume = {4}, number = {1}, pages = {4}, year = {2012}, url = {http://repository.cmu.edu/cgi/viewcontent.cgi?article = 1065&context = jpc} } @article{KST12, title = {Private convex empirical risk minimization and high-dimensional regression}, author = {Kifer, Daniel and Smith, Adam and Thakurta, Abhradeep}, journal = jmlr, volume = {1}, pages = {41}, year = {2012}, url = {http://jmlr.org/proceedings/papers/v23/kifer12/kifer12.pdf} } @inproceedings{CSS12, title = {Near-optimal differentially private principal components}, author = {Chaudhuri, Kamalika and Sarwate, Anand and Sinha, Kaushik}, booktitle = nips12, pages = {998--1006}, url = {http://books.nips.cc/papers/files/nips25/NIPS2012_0482.pdf}, year = {2012} } @inproceedings{DJW13, title = {Local privacy and statistical minimax rates}, author = {Duchi, John C and Jordan, Michael I. and Wainwright, Martin J.}, booktitle = focs13, url = {http://www.cs.berkeley.edu/~jduchi/projects/DuchiJoWa13_focs.pdf}, year = {2013} } @inproceedings{TS13, title = {(Nearly) Optimal Algorithms for Private Online Learning in Full-information and Bandit Settings}, author = {Thakurta, Abhradeep G. and Smith, Adam}, booktitle = nips13, pages = {2733--2741}, url = {http://media.nips.cc/nipsbooks/nipspapers/paper_files/nips26/1270.pdf}, year = {2013} } @inproceedings{FS95, title = {A desicion-theoretic generalization of on-line learning and an application to boosting}, author = {Freund, Yoav and Schapire, Robert E.}, booktitle = colt95, pages = {23--37}, year = {1995}, organization = springer } @inproceedings{RR10, author = {Aaron Roth and Tim Roughgarden}, title = {Interactive privacy via the median mechanism}, booktitle = stoc10, pages = {765--774}, url = {http://arxiv.org/abs/0911.1813}, year = 2010 } @inproceedings{GHRU11, title = {Privately releasing conjunctions and the statistical query barrier}, author = {Gupta, Anupam and Hardt, Moritz and Roth, Aaron and Ullman, Jonathan}, booktitle = stoc11, pages = {803--812}, url = {http://arxiv.org/abs/1011.1296}, year = {2011} } @inproceedings{TS13a, title = {Differentially Private Feature Selection via Stability Arguments, and the Robustness of the Lasso}, author = {Thakurta, Abhradeep G. and Smith, Adam}, booktitle = colt13, pages = {819--850}, url = {http://jmlr.org/proceedings/papers/v30/Guha13.pdf}, year = {2013} } @inproceedings{DL09, title = {Differential privacy and robust statistics}, author = {Dwork, Cynthia and Lei, Jing}, booktitle = stoc09, pages = {371--380}, year = {2009}, url = {http://research.microsoft.com/pubs/80239/dl09.pdf}, } @article{LW94, title = {The Weighted Majority Algorithm}, author = {Littlestone, N. and Warmuth, Manfred K.}, journal = ic, volume = {108}, number = {2}, pages = {212--261}, year = {1994}, publisher = elsevier, url = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber = 63487} } @article{PST95, title = {Fast approximation algorithms for fractional packing and covering problems}, author = {Plotkin, Serge A. and Shmoys, David B. and Tardos, {\'E}va}, journal = mor, volume = {20}, number = {2}, pages = {257--301}, year = {1995}, publisher = informs, } @inproceedings{AK07, title = {A combinatorial, primal-dual approach to semidefinite programs}, author = {Arora, Sanjeev and Kale, Satyen}, booktitle = stoc07, pages = {227--236}, year = {2007}, url = {http://dl.acm.org/citation.cfm?id=1250823} } @inproceedings{CHRMM10, title = {Optimizing linear counting queries under differential privacy}, author = {Li, Chao and Hay, Michael and Rastogi, Vibhor and Miklau, Gerome and Mc{G}regor, Andrew}, booktitle = pods10, pages = {123--134}, year = {2010}, url = {http://arxiv.org/abs/0912.4742} } @inproceedings{LM12, title = {An adaptive mechanism for accurate query answering under differential privacy}, author = {Li, Chao and Miklau, Gerome}, journal = vldb12, volume = {5}, number = {6}, pages = {514--525}, year = {2012}, url = {http://arxiv.org/abs/1202.3807} } @inproceedings{CPSY12, author = {Grigory Yaroslavtsev and Graham Cormode and Cecilia M. Procopiuc and Divesh Srivastava}, title = {Accurate and efficient private release of datacubes and contingency tables}, booktitle = icde13, year = {2013}, pages = {745--756}, url = {http://doi.ieeecomputersociety.org/10.1109/ICDE.2013.6544871} } @inproceedings{CV13, title = {A Stability-based Validation Procedure for Differentially Private Machine Learning}, author = {Chaudhuri, Kamalika and Vinterbo, Staal A.}, booktitle = nips13, pages = {2652--2660}, year = {2013}, url = {http://papers.nips.cc/paper/5014-a-stability-based-validation-procedure-for-differentially-private-machine-learning.pdf} } @article{HW01, title = {Tracking the best linear predictor}, author = {Herbster, Mark and Warmuth, Manfred K.}, journal = jmlr, volume = {1}, pages = {281--309}, url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.90.7354&rep=rep1&type=pdf}, year = {2001} } @inproceedings{DworkSurvey, title = {Differential privacy: A survey of results}, author = {Dwork, Cynthia}, booktitle = tamc08, pages = {1--19}, year = {2008}, url = {http://research.microsoft.com/apps/pubs/default.aspx?id=74339}, publisher = springer } @inproceedings{NS-social, title = {De-anonymizing social networks}, author = {Narayanan, Arvind and Shmatikov, Vitaly}, booktitle = sp09, pages = {173--187}, url = {http://arxiv.org/abs/0903.3276}, year = {2009} } @inproceedings{DNT14, title = {Using Convex Relaxations for Efficiently and Privately Releasing Marginals}, author = {Dwork, Cynthia and Nikolov, Aleksandar and Talwar, Kunal}, booktitle = socg14, pages = {261}, year = {2014}, url = {http://arxiv.org/abs/1308.1385} } @inproceedings{TUV12, title = {Faster algorithms for privately releasing marginals}, author = {Thaler, Justin and Ullman, Jonathan and Vadhan, Salil}, booktitle = icalp12, pages = {810--821}, year = {2012}, url = {http://arxiv.org/abs/1205.1758} } @article{GHRU13, title = {Privately releasing conjunctions and the statistical query barrier}, author = {Gupta, Anupam and Hardt, Moritz and Roth, Aaron and Ullman, Jonathan}, journal = siamjc, volume = {42}, number = {4}, pages = {1494--1520}, year = {2013}, url = {http://epubs.siam.org/doi/abs/10.1137/110857714} } @inproceedings{DunfieldP04, author = {Joshua Dunfield and Frank Pfenning}, title = {Tridirectional typechecking}, booktitle = popl04, pages = {281--292}, year = 2004, url = {http://www.cs.cmu.edu/~joshuad/papers/tridirectional-typechecking/Dunfield04_tridirectional.pdf} } @article{Meyer92, title = {Applying ``{D}esign by contract''}, author = {Meyer, Bertrand}, journal = {Computer}, volume = {25}, number = {10}, pages = {40--51}, year = {1992}, publisher = {IEEE}, url = {http://www-public.int-evry.fr/~gibson/Teaching/CSC7322/ReadingMaterial/Meyer92.pdf} } @inproceedings{Vazou+14:ICFP, author = {N. Vazou and E. L. Seidel and R. Jhala and D. Vytiniotis and S. {P}eyton-{J}ones}, title = {{Refinement Types for Haskell}}, booktitle = icfp14, year = {2014}, url = {http://goto.ucsd.edu/~nvazou/refinement_types_for_haskell.pdf} } @inproceedings{NR99, title = {Algorithmic mechanism design}, author = {Nisan, Noam and Ronen, Amir}, booktitle = stoc99, pages = {129--140}, year = {1999}, url = {http://www.cs.yale.edu/homes/jf/nisan-ronen.pdf} } @book{NRTV07, title = {Algorithmic game theory}, author = {Nisan, Noam and Roughgarden, Tim and Tardos, Eva and Vazirani, Vijay V}, year = {2007}, publisher = cup } @article{BBHM08, title = {Reducing mechanism design to algorithm design via machine learning}, author = {Balcan, {M}aria-{F}lorina and Blum, Avrim and Hartline, Jason D and Mansour, Yishay}, journal = {Journal of Computer and System Sciences}, volume = {74}, number = {8}, pages = {1245--1270}, year = {2008}, publisher = elsevier, url = {http://www.cs.cmu.edu/~ninamf/papers/ml_md_bbhm.pdf} } @inproceedings{DD09, title = {On the power of randomization in algorithmic mechanism design}, author = {Dobzinski, Shahar and Dughmi, Shaddin}, booktitle = focs09, pages = {505--514}, url = {http://arxiv.org/abs/0904.4193} } @article{DugR14, title = {Black-box randomized reductions in algorithmic mechanism design}, author = {Dughmi, Shaddin and Roughgarden, Tim}, journal = siamjc, volume = {43}, number = {1}, pages = {312--336}, year = {2014}, url = {http://theory.stanford.edu/~tim/papers/blackbox.pdf} } @inproceedings{CIL12, title = {On the limits of black-box reductions in mechanism design}, author = {Chawla, Shuchi and Immorlica, Nicole and Lucier, Brendan}, booktitle = stoc12, year = {2012}, url = {http://arxiv.org/abs/1109.2067} } @inproceedings{HL10, title = {Bayesian algorithmic mechanism design}, author = {Hartline, Jason D and Lucier, Brendan}, booktitle = stoc10, pages = {301--310}, year = {2010}, url = {http://arxiv.org/abs/0909.4756} } @inproceedings{Ramsey:2002, Author = {Ramsey, Norman and Pfeffer, Avi}, Booktitle = popl02, Pages = {154--165}, Title = {Stochastic lambda calculus and monads of probability distributions}, Year = {2002}, url = {http://www.cs.tufts.edu/~nr/pubs/pmonad.pdf} } @inproceedings{Park:2005, author = {Sungwoo Park and Frank Pfenning and Sebastian Thrun}, title = {A probabilistic language based upon sampling functions}, booktitle = popl05, year = {2005}, pages = {171--182}, url = {https://www.cs.cmu.edu/~fp/papers/popl05.pdf} } @article{Hurd:2005, Author = {Hurd, Joe and {M}c{I}ver, Annabelle and Morgan, Carroll}, Journal = tcs, Number = {1}, Pages = {96--112}, Title = {Probabilistic guarded commands mechanized in {HOL}}, Volume = {346}, Year = {2005}, url = {http://www.cse.unsw.edu.au/~carrollm/probs/Papers/Hurd-05.pdf} } @book{McIver:2005, Author = {{M}c{I}ver, A. and Morgan, C.}, Publisher = springer, Series = {Monographs in Computer Science}, Title = {Abstraction, Refinement, and Proof for Probabilistic Systems}, Year = {2005}} @inproceedings{Borgstrom:2011, author = {Johannes Borgstr{\"o}m and Andrew D Gordon and Michael Greenberg and James Margetson and Jurgen Van Gael}, title = {Measure Transformer Semantics for Bayesian Machine Learning}, booktitle = esop11, year = {2011}, pages = {77--96}, url = {http://cis.upenn.edu/~mgree/papers/esop2011_mts.pdf} } @inproceedings{Kiselyov:2009, author = {Oleg Kiselyov and {C}hung-{C}hieh Shan}, title = {Embedded Probabilistic Programming}, booktitle = {DSL}, year = {2009}, pages = {360--384} } @inproceedings{Goodman:2013, author = {Noah D Goodman}, title = {The principles and practice of probabilistic programming}, booktitle = popl13, year = {2013}, pages = {399--402}, url = {https://web.stanford.edu/~ngoodman/papers/POPL2013-abstract.pdf} } @inproceedings{Sampson+14, title = {Expressing and verifying probabilistic assertions}, author = {Sampson, Adrian and Panchekha, Pavel and Mytkowicz, Todd and {M}c{K}inley, Kathryn S and Grossman, Dan and Ceze, Luis}, booktitle = pldi14, pages = {14}, year = {2014}, url = {http://research.microsoft.com/pubs/211410/passert-pldi2014.pdf} } @Inproceedings {Bornholt+14, author = {James Bornholt and Todd Mytkowicz and Kathryn S {M}c{K|inley}}, booktitle = asplos14, title = {Uncertain$\langle$T$\rangle$: A First-Order Type for Uncertain Data}, year = {2014}, url = {http://research.microsoft.com/pubs/208236/asplos077-bornholtA.pdf} } @article{Giry82, author = {Giry, Mich\`{e}le}, journal = {Categorical Aspects of Topology and Analysis}, pages = {68--85}, title = {{A categorical approach to probability theory}}, year = {1982}, } @inproceedings{FreemanP91, title = {Refinement types for {ML}}, author = {Freeman, Tim and Pfenning, Frank}, booktitle = pldi91, pages = {268--277}, year = {1991}, url = {https://www.cs.cmu.edu/~fp/papers/pldi91.pdf} } @inproceedings{BBFGM08, author = "J. Bengtson and K. Bhargavan and C. Fournet and A. D. Gordon and S. Maffeis", title = "Refinement types for secure implementations", booktitle = csf08, year = 2008, url = {http://prosecco.gforge.inria.fr/personal/karthik/pubs/refinement-types-for-secure-implementations-proceedings-csf08.pdf} } @inproceedings{fstar, author = {Swamy, Nikhil and Chen, Juan and Fournet, C{\'e}dric and Strub, {P}ierre-{Y}ves and Bhargavan, Karthikeyan and Yang, Jean}, title = {Secure distributed programming with value-dependent types}, booktitle = icfp11, year = 2011, url = {http://research.microsoft.com/pubs/150012/icfp-camera-ready.pdf} } @inproceedings{liquid, title = {Liquid types}, author = {Rondon, Patrick M and Kawaguci, Ming and Jhala, Ranjit}, booktitle = pldi08, pages = {159--169}, year = {2008}, url = {http://goto.ucsd.edu/~rjhala/papers/liquid_types.pdf} } @inproceedings{rfstar, title = {Probabilistic relational verification for cryptographic implementations}, author = {Barthe, Gilles and Fournet, C{\'e}dric and Gr{\'e}goire, Benjamin and Strub, {P}ierre-{Y}ves and Swamy, Nikhil and Zanella{-}B{\'e}guelin, Santiago}, booktitle = popl14, pages = {193--206}, year = {2014}, url = {http://research.microsoft.com/en-us/um/people/nswamy/papers/rfstar.pdf} } @INPROCEEDINGS{polymonad, TITLE = {Polymonadic Programming}, AUTHOR = {Michael Hicks and Gavin Bierman and Nataliya Guts and Daan Leijen and Nikhil Swamy}, BOOKTITLE = mfps14, YEAR = 2014, url = {http://arxiv.org/abs/1406.2060} } @inproceedings{Dwork06, Author = {Dwork, Cynthia}, Booktitle = icalp06, Pages = {1--12}, Title = {Differential Privacy}, Year = {2006}, url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.83.7534&rep=rep1&type=pdf} } @inproceedings{Benton04, Author = {Benton, Nick}, Booktitle = popl04, Pages = {14--25}, Title = {Simple relational correctness proofs for static analyses and program transformations}, Year = {2004}, url = {http://research.microsoft.com/en-us/um/people/nick/correctnessfull.pdf} } @inproceedings{AmtoftB04, author = {Torben Amtoft and Anindya Banerjee}, title = {Information Flow Analysis in Logical Form}, booktitle = sas04, pages = {100--115}, publisher = springer, series = lncs, volume = {3148}, year = {2004}, url = {http://software.imdea.org/~ab/Publications/ifalftr.pdf} } @inproceedings{BartheGZ09, Author = {Barthe, Gilles and Gr{\'e}goire, Benjamin and Zanella{-}B{\'e}guelin, Santiago}, Booktitle = popl09, Pages = {90--101}, Title = {Formal Certification of Code-Based Cryptographic Proofs}, Year = {2009}, url = {http://research.microsoft.com/pubs/185309/Zanella.2009.POPL.pdf} } @inproceedings{BartheDGKZ13, author = {Barthe, Gilles and Danezis, George and Gr{\'e}goire, Benjamin and Kunz, C{\'e}sar and Zanella{-}B{\'e}guelin Santiago}, title = {Verified Computational Differential Privacy with Applications to Smart Metering}, booktitle = csf13, year = {2013}, pages = {287--301}, url = {http://www0.cs.ucl.ac.uk/staff/G.Danezis/papers/easypriv.pdf} } @inproceedings{DBLP:journals/corr/BaiTG14, author = {Wei Bai and Emmanuel M Tadjouddine and Yu Guo}, title = {Enabling Automatic Certification of Online Auctions}, booktitle = fesca14, series = {EPTCS}, volume = {147}, year = {2014}, pages = {123--132}, url = {http://dx.doi.org/10.4204/EPTCS.147.9}, } @inproceedings{DBLP:conf/facs2/BaiTPG13, author = {Wei Bai and Emmanuel M Tadjouddine and Terry R Payne and Sheng-Uei Guan}, title = {A Proof-Carrying Code Approach to Certificate Auction Mechanisms}, booktitle = {FACS}, year = {2013}, pages = {23--40}, url = {http://dx.doi.org/10.1007/978--3-319--07602--7_4}, publisher = springer, series = lncs, volume = {8348}, } @inproceedings{DBLP:conf/ceemas/TadjouddineG07, author = {Emmanuel M Tadjouddine and Frank Guerin}, title = {Verifying Dominant Strategy Equilibria in Auctions}, booktitle = ceemas07, year = {2007}, pages = {288--297}, url = {http://dx.doi.org/10.1007/978--3-540--75254--7_29}, publisher = springer, series = lncs, volume = {4696}, } @article{DBLP:journals/ipl/Vestergaard06, author = {Ren{\'e} Vestergaard}, title = {A constructive approach to sequential Nash equilibria}, journal = {Inf. Process. Lett.}, volume = {97}, number = {2}, year = {2006}, pages = {46--51}, url = {http://dx.doi.org/10.1016/j.ipl.2005.09.010}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{Roux:2009, author = {Le Roux, St{\'e}phane}, title = {Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence}, booktitle = tphol09, year = {2009} } @techreport{BUCS-TR-2008-026, author = {Andrei Lapets and Alex Levin and David Parkes}, title = {{A Typed Truthful Language for One-dimensional Truthful Mechanism Design}}, number = {BUCS-TR-2008--026}, year = {2008}, institution = {Boston University}, url = {http://cs-people.bu.edu/lapets/resource/typed-ec-mech.pdf} } @misc{Fang14, author = {Ye Fang and Swarat Chaudhuri and Moshe Vardi}, title = {{Computer-aided mechanism design}}, howpublished = {Poster at POPL'14}, year = {2014} } @inproceedings{CasinghinoSW14, author = {Chris Casinghino and Vilhelm Sj\"{o}berg and Stephanie Weirich}, title = {Combining Proofs and Programs in a Dependently Typed Langauge}, booktitle = popl14, year = {2014}, url = {http://www.seas.upenn.edu/~ccasin/papers/combining-TR.pdf} } @inproceedings{DBLP:conf/mkm/0002CKMRWW13, author = {Christoph Lange and Marco B Caminati and Manfred Kerber and Till Mossakowski and Colin Rowat and Makarius Wenzel and Wolfgang Windsteiger}, title = {A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory}, booktitle = {MKM/Calculemus/DML}, publisher = springer, series = lncs, volume = {7961}, year = {2013}, pages = {200--215}, url = {http://dx.doi.org/10.1007/978--3-642--39320--4_13} } @article{DBLP:journals/cacm/ChaudhuriGL12, author = {Swarat Chaudhuri and Sumit Gulwani and Roberto Lublinerman}, title = {Continuity and robustness of programs}, journal = cacm, volume = {55}, number = {8}, year = {2012}, pages = {107--115}, url = {http://dl.acm.org/citation.cfm?id=2240262} } @article{BartheDR04, title = {Secure information flow by self-composition}, author = {Barthe, Gilles and D'Argenio, Pedro R and Rezk, Tamara}, journal = mscs, volume = {21}, number = {06}, pages = {1207--1252}, year = {2011}, publisher = cup, url = {http://www-sop.inria.fr/lemme/Tamara.Rezk/publication/Barthe-DArgenio-Rezk-Journal.pdf} } @inproceedings{ZaksP08, author = {Anna Zaks and Amir Pnueli}, title = {{CoVaC}: Compiler Validation by Program Analysis of the Cross-Product}, booktitle = fm08, pages = {35--51}, publisher = springer, series = lncs, volume = {5014}, year = {2008}, url = {http://llvm.org/pubs/2008-05-CoVaC.pdf} } @inproceedings{TerauchiA05, Author = {Terauchi, Tachio and Aiken, Alex}, Booktitle = sas05, Pages = {352--367}, Publisher = springer, Series = lncs, Title = {Secure Information Flow as a Safety Problem}, Volume = {3672}, Year = {2005}, url = {http://theory.stanford.edu/~aiken/publications/papers/sas05b.pdf} } @inproceedings{BartheCK11, author = {Gilles Barthe and Juan Manuel Crespo and C{\'e}sar Kunz}, title = {Relational Verification Using Product Programs}, booktitle = fm11, year = {2011}, pages = {200--214}, url = {http://software.imdea.org/~ckunz/rellog/long-rellog.pdf}, } @inproceedings{BartheCK13, author = {Gilles Barthe and Juan Manuel Crespo and C{\'e}sar Kunz}, title = {Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification}, booktitle = lfcompsci13, year = {2013}, pages = {29--43}, url = {http://dx.doi.org/10.1007/978--3-642--35722--0_3}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DBLP:conf/esop/KnowlesF07, author = {Kenneth Knowles and Cormac Flanagan}, title = {Type Reconstruction for General Refinement Types}, booktitle = esop07, year = {2007}, pages = {505--519}, url = {http://users.soe.ucsc.edu/~cormac/papers/esop07.pdf} } @inproceedings{DBLP:conf/esop/WadlerF09, author = {Philip Wadler and Robert Bruce Findler}, title = {Well-Typed Programs Can't Be Blamed}, booktitle = esop09, year = {2009}, pages = {1--16}, url = {http://homepages.inf.ed.ac.uk/wadler/papers/blame/blame.pdf} } @inproceedings{DBLP:conf/popl/GreenbergPW10, author = {Michael Greenberg and Benjamin C. Pierce and Stephanie Weirich}, title = {Contracts made manifest}, booktitle = popl10, year = {2010}, pages = {353--364}, url = {http://www.cis.upenn.edu/~bcpierce/papers/contracts-popl.pdf} } @inproceedings{DBLP:conf/sfp/GronskiF07, author = {Jessica Gronski and Cormac Flanagan}, title = {Unifying Hybrid Types and Contracts}, booktitle = tfp07, year = {2007}, pages = {54--70}, url = {https://sage.soe.ucsc.edu/tfp07-gronski-flanagan.pdf} } @inproceedings{OngR11, title = {Verifying higher-order functional programs with pattern-matching algebraic data types}, author = {Ong, C-H Luke and Ramsay, Steven James}, booktitle = popl11, pages = {587--598}, year = {2011}, url = {https://www.cs.ox.ac.uk/files/3721/main.pdf} } @misc{Pierce:2012, author = {Benjamin C. Pierce}, title = {Differential Privacy in the Programming Languages Community}, year = {2012}, howpublished = {Invited tutorial at DIMACS Workshop on Recent Work on Differential Privacy across Computer Science} } @inproceedings{FindlerF02, author = {Robert Bruce Findler and Matthias Felleisen}, title = {Contracts for higher-order functions}, booktitle = icfp02, year = {2002}, pages = {48--59}, url = {http://www.eecs.northwestern.edu/~robby/pubs/papers/ho-contracts-techreport.pdf} } @INPROCEEDINGS{Augustsson98, author = {Lennart Augustsson}, title = {Cayenne -- a Language With Dependent Types}, booktitle = icfp98, year = {1998}, pages = {239--250}, url = {http://link.springer.com/chapter/10.1007%2F10704973_6} } @article{Brady13, author = {Edwin Brady}, title = {Idris, a general-purpose dependently typed programming language: Design and implementation}, journal = jfp, volume = {23}, number = {5}, year = {2013}, pages = {552--593}, url = {http://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf} } @incollection{epigram, title = {Epigram: Practical programming with dependent types}, author = {{M}c{B}ride, Conor}, booktitle = {Advanced Functional Programming}, pages = {130--170}, year = {2005}, publisher = springer, url = {http://cs.ru.nl/~freek/courses/tt-2010/tvftl/epigram-notes.pdf} } @inproceedings{Vytiniotis+13, author = {Vytiniotis, Dimitrios and Peyton Jones, Simon and Claessen, Koen and Ros{\'e}n, Dan}, title = {HALO: Haskell to Logic Through Denotational Semantics}, booktitle = popl13, year = {2013}, url = {http://research.microsoft.com/en-us/people/dimitris/hcc-popl.pdf} } @INPROCEEDINGS{Flanagan06, author = {Jessica Gronski and Kenneth Knowles and Aaron Tomb and Stephen N Freund and Cormac Flanagan}, title = {Sage: Hybrid checking for flexible specifications}, booktitle = {Scheme and Functional Programming Workshop}, year = {2006}, pages = {93--104}, url = {http://galois.com/wp-content/uploads/2014/07/pub_AT_SAGEHybridChecking.pdf} } @inproceedings{EignerM13, author = {Fabienne Eigner and Matteo Maffei}, title = {Differential Privacy by Typing in Security Protocols}, booktitle = csf13, year = {2013}, pages = {272--286}, url = {http://sps.cs.uni-saarland.de/publications/dp_proto_long.pdf} } @inproceedings{GordonHNR14, author = {Andrew D Gordon and Thomas A Henzinger and Aditya V Nori and Sriram K Rajamani}, title = {Probabilistic programming}, booktitle = icse14, year = {2014}, pages = {167--181}, url = {http://research.microsoft.com/pubs/208585/fose-icse2014.pdf} } @inproceedings{DaviesP00, author = {Rowan Davies and Frank Pfenning}, title = {Intersection types and computational effects}, booktitle = icfp00, year = {2000}, pages = {198--208}, url = {http://www.cs.cmu.edu/~fp/papers/icfp00.pdf} } @inproceedings{XiP99, author = {Hongwei Xi and Frank Pfenning}, title = {Dependent Types in Practical Programming}, booktitle = popl99, year = {1999}, pages = {214--227}, url = {http://www.cs.cmu.edu/~fp/papers/popl99.pdf} } @inproceedings{DMNS06, author = {Cynthia Dwork and Frank McSherry and Kobbi Nissim and Adam D. Smith}, title = {Calibrating Noise to Sensitivity in Private Data Analysis}, booktitle = tcc06, volume = 3876, series = lncs, pages = {265--284}, year = {2006}, url = {http://dx.doi.org/10.1007/11681878_14}, doi = {10.1007/11681878_14}, publisher = springer } @inproceedings{Tschantz201161, title = {Formal Verification of Differential Privacy for Interactive Systems}, author = {Tschantz, Michael Carl and Kaynar, Dilsun and Datta, Anupam}, booktitle = mfps11, series = entcs, volume = 276, pages = {61--79}, year = 2011, url = {http://arxiv.org/pdf/1101.2819v1}, publisher = elsevier } @article{GHKSW06, title = {Competitive auctions}, author = {Goldberg, Andrew V and Hartline, Jason D and Karlin, Anna R and Saks, Michael and Wright, Andrew}, journal = geb, volume = {55}, number = {2}, year = {2006}, pages = {242--269}, url = {http://www.ime.usp.br/~yw/papers/games/goldberg2008-competitive-auctions.pdf}, publisher = {Elsevier} } @article{mu2008truthful, title = {Truthful approximation mechanisms for restricted combinatorial auctions}, author = {Mu'{A}lem, Ahuva and Nisan, Noam}, journal = geb, volume = {64}, number = {2}, pages = {612--631}, year = {2008}, url = {http://authors.library.caltech.edu/13158/1/MUAgeb08preprint.pdf}, publisher = {Elsevier} } @inproceedings{milgrom2014deferred, title = {Deferred-acceptance auctions and radio spectrum reallocation}, author = {Milgrom, Paul and Segal, Ilya}, booktitle = ec14, pages = {185--186}, year = {2014}, url = {http://web.stanford.edu/~isegal/heuristic.pdf} } @article{CKRW14, author = {Rachel Cummings and Michael Kearns and Aaron Roth and Zhiwei Steven Wu}, title = {Privacy and Truthful Equilibrium Selection for Aggregative Games}, journal = {CoRR}, year = {2014}, volume = {abs/1407.7740}, url = {http://arxiv.org/abs/1407.7740}, timestamp = {Sun, 26 Oct 2014 15:36:31 +0100}, biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/CummingsKRW14}, bibsource = {dblp computer science bibliography, http://dblp.org} } @inproceedings{HK12, title = {The exponential mechanism for social welfare: Private, truthful, and nearly optimal}, author = {Huang, Zhiyi and Kannan, Sampath}, booktitle = focs12, pages = {140--149}, year = {2012}, url = {http://arxiv.org/abs/1204.1255} } @inproceedings{zinkevich, author = {Martin Zinkevich}, title = {Online Convex Programming and Generalized Infinitesimal Gradient Ascent}, booktitle = icml03, year = {2003}, pages = {928--936}, url = {http://www.aaai.org/Library/ICML/2003/icml03-120.php}, timestamp = {Thu, 16 Oct 2014 21:45:09 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/icml/Zinkevich03}, bibsource = {dblp computer science bibliography, http://dblp.org} } @article{JKT11, title = {Differentially private online learning}, author = {Jain, Prateek and Kothari, Pravesh and Thakurta, Abhradeep Guha}, journal = {arXiv preprint arXiv:1109.0105}, year = {2011}, url = {http://arxiv.org/abs/1109.0105} } @inproceedings{JT14, title = {({N}ear) Dimension Independent Risk Bounds for Differentially Private Learning}, author = {Jain, Prateek and Thakurta, Abhradeep Guha}, booktitle = icml14, pages = {476--484}, year = {2014}, url = {http://jmlr.org/proceedings/papers/v32/jain14.pdf} } @inproceedings{BST14, title = {Differentially Private Empirical Risk Minimization: Efficient Algorithms and Tight Error Bounds}, author = {Bassily, Raef and Smith, Adam and Thakurta, Abhradeep Guha}, booktitle = focs14, year = {2014}, url = {http://arxiv.org/abs/1405.7085} } @article{dualdecomp, title = {Distributed optimization and statistical learning via the alternating direction method of multipliers}, author = {Boyd, Stephen and Parikh, Neal and Chu, Eric and Peleato, Borja and Eckstein, Jonathan}, journal = {Foundations and Trends{\textregistered} in Machine Learning}, volume = {3}, number = {1}, pages = {1--122}, year = {2011}, publisher = {Now Publishers Inc.}, url = {https://web.stanford.edu/~boyd/papers/pdf/admm_distr_stats.pdf} } @inproceedings{NST12, title = {Approximately optimal mechanism design via differential privacy}, author = {Nissim, Kobbi and Smorodinsky, Rann and Tennenholtz, Moshe}, booktitle = itcs12, pages = {203--213}, year = {2012}, url = {http://arxiv.org/abs/1004.2888} } @inproceedings{CCKMV13, title = {Truthful mechanisms for agents that value privacy}, author = {Chen, Yiling and Chong, Stephen and Kash, Ian A and Moran, Tal and Vadhan, Salil}, booktitle = ec13, pages = {215--232}, year = {2013}, url = {http://arxiv.org/abs/1111.5472} } @inproceedings{Xia13, title = {Is privacy compatible with truthfulness?}, author = {Xiao, David}, booktitle = itcs13, pages = {67--86}, year = {2013}, url = {https://eprint.iacr.org/2011/005} } @inproceedings{IOh01, title = {{BI} as an assertion language for mutable data structures}, author = {Ishtiaq, Samin S and O'Hearn, Peter W}, booktitle = popl01, year = 2001, url = {http://dl.acm.org/citation.cfm?id=375719}, pages = {14--26} } @inproceedings{OhRY01, title = {Local reasoning about programs that alter data structures}, author = {O'Hearn, Peter W and Reynolds, John and Yang, Hongseok}, booktitle = csl01, year = 2001, url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.29.1331&rep=rep1&type=pdf}, pages = {1--19} } @inproceedings{DOhY06, title = {A local shape analysis based on separation logic}, author = {Distefano, Dino and O'Hearn, Peter W and Yang, Hongseok}, booktitle = tacas06, year = 2006, url = {http://dl.acm.org/citation.cfm?id=2182039}, pages = {287--302} } @inproceedings{BCCC07, title = {Shape analysis for composite data structures}, author = {Berdine, Josh and Calcagno, Cristiano and Cook, Byron and Distefano, Dino and O'Hearn, Peter W and Wies, Thomas and Yang, Hongseok}, booktitle = cav07, pages = {178--192}, url = {http://research.microsoft.com/pubs/73868/safcds.pdf}, year = {2007} } @article{Reynolds01, title = {Intuitionistic reasoning about shared mutable data structure}, author = {Reynolds, John C}, journal = {Millennial perspectives in computer science}, volume = {2}, number = {1}, year = 2001, url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.11.5999&rep=rep1&type=pdf}, pages = {303--321} } @inproceedings{Reynolds02, title = {Separation logic: A logic for shared mutable data structures}, author = {Reynolds, John C}, booktitle = lics02, year = 2002, pages = {55--74} } @article{Burstall72, title = {Some techniques for proving correctness of programs which alter data structuers}, author = {Rodnew M Burstall}, journal = {Machine Intelligence}, volume = {7}, number = {3}, year = 1972, pages = {23--50} } @inproceedings{smallfoot, title = {Smallfoot: Modular automatic assertion checking with separation logic}, author = {Berdine, Josh and Calcagno, Cristiano and O'Hearn, Peter W}, booktitle = fmco06, pages = {115--137}, url = {http://research.microsoft.com/pubs/67598/smallfoot.pdf}, year = {2006} } @incollection{VP07, title = {A marriage of rely/guarantee and separation logic}, author = {Vafeiadis, Viktor and Parkinson, Matthew}, booktitle = concur07, pages = {256--271}, url = {http://www.cl.cam.ac.uk/~mjp41/RGSep.pdf}, year = 2007 } @inproceedings{NDQC07, title = {Automated verification of shape and size properties via separation logic}, author = {Nguyen, Huu Hai and David, Cristina and Qin, Shengchao and Chin, Wei-Ngan}, booktitle = vmcai07, pages = {251--266}, url = {http://link.springer.com/chapter/10.1007%2F978-3-540-69738-1_18}, year = {2007} } @inproceedings{BCOh04, title = {A decidable fragment of separation logic}, author = {Berdine, Josh and Calcagno, Cristiano and O'Hearn, Peter W}, booktitle = fsttcs04, pages = {97--109}, url = {http://research.microsoft.com/pubs/73583/unroll_collapse.pdf}, year = 2004 } @incollection{HAN08, title = {Oracle semantics for concurrent separation logic}, author = {Hobor, Aquinas and Appel, Andrew W and Nardelli, Francesco Zappa}, booktitle = {Programming Languages and Systems (with ESOP)}, pages = {353--367}, url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.116.4226&rep=rep1&type=pdf}, year = {2008} } @inproceedings{Krebbers14, title = {An operational and axiomatic semantics for non-determinism and sequence points in {C}}, author = {Krebbers, Robbert}, booktitle = popl14, pages = {101--112}, url = {http://robbertkrebbers.nl/research/articles/expressions.pdf}, year = {2014} } @article{OhP99, title = {The logic of bunched implications}, author = {O'Hearn, Peter W and Pym, David J}, journal = bsl, pages = {215--244}, url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.27.4742&rep=rep1&type=pdf}, year = {1999} } @article{POhY04, title = {Possible worlds and resources: The semantics of {BI}}, author = {Pym, David J and O'Hearn, Peter W and Yang, Hongseok}, journal = tcs, volume = {315}, number = {1}, pages = {257--305}, year = {2004}, url = {http://www.sciencedirect.com/science/article/pii/S0304397503006248}, publisher = {Elsevier} } @inproceedings{BCOh05, title = {Symbolic execution with separation logic}, author = {Berdine, Josh and Calcagno, Cristiano and O'Hearn, Peter W}, booktitle = aplas05, url = {http://research.microsoft.com/pubs/64175/execution.pdf}, year = {2005} } @inproceedings{Cousout77, title = {Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints}, author = {Cousot, Patrick and Cousot, Radhia}, booktitle = popl77, pages = {238--252}, url = {http://www.di.ens.fr/~cousot/publications.www/CousotCousot-POPL-77-ACM-p238--252-1977.pdf}, year = {1977} } @article{Cousout96, title = {Abstract interpretation}, author = {Cousot, Patrick}, journal = {{ACM} Computing Surveys}, volume = {28}, number = {2}, pages = {324--328}, year = {1996}, url = {http://dl.acm.org/citation.cfm?id=234740}, } @inproceedings{dwork2010pan, title = {Pan-Private Streaming Algorithms.}, author = {Dwork, Cynthia and Naor, Moni and Pitassi, Toniann and Rothblum, Guy N and Yekhanin, Sergey}, booktitle = itcs10, pages = {66--80}, url = {http://www.cs.toronto.edu/~toni/Papers/panprivacy.pdf}, year = {2010} } @inproceedings{recommender, title = {Differentially private recommender systems: building privacy into the net}, author = {McSherry, Frank and Mironov, Ilya}, booktitle = kdd09, pages = {627--636}, year = {2009}, url = {http://research.microsoft.com/pubs/80511/netflixprivacy.pdf} } @book{cvxbook, author = {Boyd, Stephen and Vandenberghe, Lieven}, title = {Convex Optimization}, year = {2004}, isbn = {0521833787}, publisher = cup, } @book{concentration-book, title = {Concentration of measure for the analysis of randomized algorithms}, author = {Dubhashi, Devdatt P and Panconesi, Alessandro}, year = {2009}, publisher = cup } @article{LovaszLocal, title = {Problems and results on 3-chromatic hypergraphs and some related questions}, author = {Erdos, Paul and Lov{\'a}sz, L{\'a}szl{\'o}}, journal = {Infinite and finite sets}, volume = {10}, pages = {609--627}, year = {1975} } @article{erdosPM, title = {Graph theory and probability}, author = {Paul Erd{\H{o}}s}, journal = {Canadian Journal of Mathematics}, volume = {11}, pages = {34--38}, year = {1959} } @inproceedings{DBLP:conf/pldi/SampsonPMMGC14, author = {Adrian Sampson and Pavel Panchekha and Todd Mytkowicz and Kathryn S McKinley and Dan Grossman and Luis Ceze}, title = {Expressing and verifying probabilistic assertions}, booktitle = pldi14, pages = {112--122}, year = {2014}, url = {http://doi.acm.org/10.1145/2594291.2594294}, } @inproceedings{DBLP:conf/pldi/CarbinKMR12, author = {Michael Carbin and Deokhwan Kim and Sasa Misailovic and Martin C Rinard}, title = {Proving acceptability properties of relaxed nondeterministic approximate programs}, booktitle = pldi12, pages = {169--180}, year = {2012}, url = {http://doi.acm.org/10.1145/2254064.2254086}, } @article{alea, title = {Proofs of randomized algorithms in {C}oq}, author = {Audebaud, Philippe and Paulin-Mohring, Christine}, journal = {Science of Computer Programming}, volume = {74}, number = {8}, pages = {568--589}, year = {2009}, publisher = elsevier } @inproceedings{DBLP:conf/pldi/SampsonPMMGC14, author = {Adrian Sampson and Pavel Panchekha and Todd Mytkowicz and Kathryn S McKinley and Dan Grossman and Luis Ceze}, title = {Expressing and verifying probabilistic assertions}, booktitle = pldi14, pages = {14}, year = {2014}, url = {http://doi.acm.org/10.1145/2594291.2594294}, } @inproceedings{DBLP:conf/pldi/CarbinKMR12, author = {Michael Carbin and Deokhwan Kim and Sasa Misailovic and Martin C Rinard}, title = {Proving acceptability properties of relaxed nondeterministic approximate programs}, booktitle = pldi12, pages = {169--180}, year = {2012}, url = {http://doi.acm.org/10.1145/2254064.2254086}, } @InProceedings{Necula97, author = "G. C. Necula", title = "Proof-carrying code", booktitle = popl97, year = "1997", pages = "106--119", } @inproceedings{BartheGHZ11, author = {Barthe, Gilles and Gr{\'e}goire, Benjamin and Heraud, Sylvain and Zanella{-}B{\'e}guelin, Santiago}, title = {Computer-Aided Security Proofs for the Working Cryptographer}, Booktitle = crypto11, year = {2011}, Pages = {71--90}, publisher = springer, series = lncs, volume = {6841}, url = {http://software.imdea.org/~szanella/Zanella.2011.CRYPTO.pdf}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{flanagan2001, title = {Avoiding exponential explosion: Generating compact verification conditions}, author = {Flanagan, Cormac and Saxe, James B}, booktitle = popl01, pages = {193--205}, year = {2001}, } @inproceedings{BartheDGKSS13, author = {Gilles Barthe and Fran{\c{c}}ois Dupressoir and Benjamin Gr{\'{e}}goire and C{\'{e}}sar Kunz and Benedikt Schmidt and Pierre{-}Yves Strub}, title = {EasyCrypt: {A} Tutorial}, booktitle = {Foundations of Security Analysis and Design {VII} - {FOSAD} 2012/2013 Tutorial Lectures}, series = lncs, volume = {8604}, pages = {146--166}, publisher = springer, year = {2013} } @article{hoare1969axiomatic, title={An axiomatic basis for computer programming}, author={Hoare, Charles Antony Richard}, journal=cacm, volume={12}, number={10}, pages={576--580}, year={1969}, } @incollection{Floyd67, author = {Floyd, Robert W.}, booktitle = {Symposium on {A}pplied {M}athematics}, publisher = {Amer. Math. Soc.}, title = {{Assigning meanings to programs}}, year = {1967} } @article{Cook:1978, Author = {Cook, S.}, Journal = siamjc, Number = {1}, Pages = {70--90}, Title = {Soundness and Completeness of an Axiom System for Program Verification}, Volume = {7}, Year = {1978} } @inproceedings{Clarkson:2008, Author = {Clarkson, M.R. and Schneider, F.B.}, Booktitle = csf08, Title = {Hyperproperties}, Year = {2008} } @InProceedings{Turing:1949, author = "Alan M. Turing", title = "Checking a Large Routine", pages = "67--69", year = "1949", URL = "http://www.turingarchive.org/browse.php/B/8", booktitle = "{Report on a Conference on High Speed Automatic Computation, June 1949}", } @inproceedings{HM07, title = {The communication complexity of uncoupled nash equilibrium procedures}, author = {Hart, Sergiu and Mansour, Yishay}, booktitle = stoc07, pages = {345--353}, year = {2007}, } @article{DGP09, title = {The complexity of computing a Nash equilibrium}, author = {Daskalakis, Constantinos and Goldberg, Paul W and Papadimitriou, Christos H}, journal = siamjc, volume = {39}, number = {1}, pages = {195--259}, year = {2009}, } @inproceedings{CS02, title = {Complexity of mechanism design}, author = {Conitzer, Vincent and Sandholm, Tuomas}, booktitle = uai02, pages = {103--110}, year = {2002}, organization = {Morgan Kaufmann Publishers Inc.} } @inproceedings{San03, title = {Automated mechanism design: A new application area for search algorithms}, author = {Sandholm, Tuomas}, booktitle = cp03, pages = {19--36}, year = {2003}, organization = springer } @inproceedings{BP14, title = {Verifiably Truthful Mechanisms}, author = {Br{\^a}nzei, Simina and Procaccia, Ariel D}, booktitle = itcs14, year = {2014} } @phdthesis{Con06, title = {Computational aspects of preference aggregation}, author = {Conitzer, Vincent}, year = {2006}, school = {IBM} } @inproceedings{HKM11, title = {Bayesian incentive compatibility via matchings}, author = {Hartline, Jason D and Kleinberg, Robert and Malekian, Azarakhsh}, booktitle = soda11, pages = {734--747}, year = {2011}, } @inproceedings{BH11, title = {Bayesian incentive compatibility via fractional assignments}, author = {Bei, Xiaohui and Huang, Zhiyi}, booktitle = soda11, pages = {720--733}, year = {2011}, } @book{Rou05, title = {Selfish routing and the price of anarchy}, author = {Roughgarden, Tim}, volume = {174}, year = {2005}, publisher = mitpress } @article{Morgan:1996, author = {Carroll Morgan and Annabelle McIver and Karen Seidel}, title = {Probabilistic Predicate Transformers}, journal = toplas, volume = {18}, number = {3}, year = {1996}, pages = {325--353} } @article{Kozen:1985, author = {D. Kozen}, title = {A Probabilistic {PDL}}, journal = jcss, volume = {30}, number = {2}, year = {1985} } @article{Morgan:1996, author = {C Morgan and A Mc{I}ver and K Seidel}, title = {Probabilistic Predicate Transformers}, journal = toplas, volume = {18}, number = {3}, year = {1996} } @article{Kozen:1985, author = {D. Kozen}, title = {A Probabilistic {PDL}}, journal = jcss, volume = {30}, number = {2}, year = {1985} } @inproceedings{TGV09, year = {2009}, booktitle = {Declarative Agent Languages and Technologies VI}, volume = {5397}, series = lncs, title = {Abstracting and Verifying Strategy-Proofness for Auction Mechanisms}, publisher = springer, author = {Tadjouddine, Emmanuel M. and Guerin, Frank and Vasconcelos, Wamberto}, pages = {197--214}, } @inproceedings{DBLP:conf/ceemas/TadjouddineG07, author = {Emmanuel M Tadjouddine and Frank Guerin}, title = {Verifying Dominant Strategy Equilibria in Auctions}, booktitle = {{CEEMAS 2007}}, year = {2007}, pages = {288--297}, publisher = springer, series = lncs, volume = {4696}, } @inproceedings{DBLP:journals/corr/BaiTG14, author = {Wei Bai and Emmanuel M Tadjouddine and Yu Guo}, title = {Enabling Automatic Certification of Online Auctions}, booktitle = {{FESCA 2014}}, series = {EPTCS}, volume = {147}, year = {2014}, pages = {123--132}, url = {http://dx.doi.org/10.4204/EPTCS.147.9}, } @incollection{DBLP:conf/mkm/0002CKMRWW13, author = {Christoph Lange and Marco B Caminati and Manfred Kerber and Till Mossakowski and Colin Rowat and Makarius Wenzel and Wolfgang Windsteiger}, title = {A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory}, booktitle = {Intelligent Computer Mathematics}, publisher = springer, series = lncs, volume = {7961}, year = {2013}, pages = {200--215}, url = {http://dx.doi.org/10.1007/978--3-642--39320--4_13}, publisher = springer } @article{DBLP:journals/ipl/Vestergaard06, author = {Ren{\'e} Vestergaard}, title = {A constructive approach to sequential Nash equilibria}, journal = {Inf. Process. Lett.}, volume = {97}, number = {2}, year = {2006}, pages = {46--51}, url = {http://dx.doi.org/10.1016/j.ipl.2005.09.010}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DBLP:conf/aaai/WooldridgeADH07, author = {Michael Wooldridge and Thomas {A}gotnes and Paul E. Dunne and Wiebe van der Hoek}, title = {Logic for Automated Mechanism Design---{A} Progress Report}, booktitle = aaai07, pages = {9--17}, year = {2007}, } @Article{Alur:2002:ATT, author = "Rajeev Alur and Thomas A. Henzinger and Orna Kupferman", title = "Alternating-time temporal logic", journal = jacm, volume = "49", number = "5", pages = "672--713", year = "2002", journal-url = "http://portal.acm.org/browse_dl.cfm?idx = J401", } @inproceedings{Gonthier13, author = {Georges Gonthier and Andrea Asperti and Jeremy Avigad and Yves Bertot and Cyril Cohen and Fran{\c{c}}ois Garillot and St{\'{e}}phane Le Roux and Assia Mahboubi and Russell O'{C}onnor and Sidi Ould Biha and Ioana Pasca and Laurence Rideau and Alexey Solovyev and Enrico Tassi and Laurent Th{\'{e}}ry}, title = {A Machine-Checked Proof of the Odd Order Theorem}, booktitle = {Interactive Theorem Proving (ITP)}, pages = {163--179}, year = {2013}, } @article{clarke71, title = {Multipart pricing of public goods}, author = {Clarke, Edward H}, journal = {Public choice}, volume = {11}, number = {1}, pages = {17--33}, year = {1971}, publisher = springer } @article{groves73, title = {Incentives in teams}, author = {Groves, Theodore}, journal = {Econometrica: Journal of the Econometric Society}, pages = {617--631}, year = {1973} } @inproceedings{Bellare:2006, author = {Bellare, Mihir and Rogaway, Phillip}, booktitle = eucrypt06, pages = {409--426}, publisher = springer, series = lncs, title = {The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs}, volume = {4004}, year = {2006}, url = {https://www.iacr.org/archive/eurocrypt2006/40040415/40040415.pdf} } @misc{Halevi:2005, author = {Halevi, Shai}, howpublished = {Cryptology ePrint Archive, Report 2005/181}, title = {A plausible approach to computer-aided cryptographic proofs}, year = {2005}, url = {https://eprint.iacr.org/2005/181.pdf} } @misc{Shoup:2004, author = {Shoup, Victor}, howpublished = {Cryptology ePrint Archive, Report 2004/332}, title = {Sequences of games: a tool for taming complexity in security proofs}, year = {2004} } @unpublished{Naumann:2009, author = {Naumann, David A}, title = {Theory for software verification}, year = {2009}, url = {http://www.cs.stevens.edu/~naumann/publications/theoryverif.pdf} } @incollection{handbook-sat, title = {Satisfiability Modulo Theories}, author = {Barrett, Clark and Sebastini, Roberto and Seshia, Sanjit A and Tinelli, Cesare}, booktitle = {Handbook of satisfiability}, volume = {185}, year = {2009}, publisher = {IOS press}, } @inproceedings{HPN11, title = {Differential Privacy Under Fire}, author = {Haeberlen, Andreas and Pierce, Benjamin C. and Narayan, Arjun}, booktitle = {USENIX Security Symposium}, year = {2011} } @article{Girard87, title = {{Linear logic}}, author = {Girard, J.Y.}, journal = tcs, volume = {50}, number = {1}, pages = {1--102}, year = {1987}, publisher = {Elsevier} } @incollection{Walker-atapl, author = {David Walker}, title = {Substructural Type Systems}, booktitle = {Advanced Topics in Types and Programming Languages}, editor = {Benjamin C. Pierce}, publisher = mitpress, year = {2005}, } @article{BLL, title = {{Bounded linear logic}}, author = {Girard, J.Y. and Scedrov, A. and Scott, P.}, journal = tcs, volume = {97}, number = {1}, pages = {1--66}, year = {1992} } @inproceedings{WrightBaker93, title = {{Usage Analysis with Natural Reduction Types}}, author = {Wright, D.A. and Baker-Finch, C.A.}, booktitle = {International Workshop on Static Analysis}, pages = {254--266}, year = {1993}, publisher = springer } @InProceedings{DalLagoHofmann09, title = "Bounded Linear Logic, Revisited", author = "Dal Lago, Ugo and Hofmann, Martin", booktitle = tlca, publisher = springer, year = "2009", volume = "5608", pages = "80--94", series = lncs, } @InProceedings{XiPfenning99, author = "Hongwei Xi and Frank Pfenning", title = "Dependent Types in Practical Programming", pages = "214--227", booktitle = popl99, year = "1999", } @InProceedings{ATS, title = "Combining programming with theorem proving", author = "Chiyan Chen and Hongwei Xi", booktitle = icfp05, year = "2005", pages = "66--77", url = "http://doi.acm.org/10.1145/1086365.1086375", } @article{McBrideMcKinna02, author = {Conor Mc{B}ride and James Mc{K}inna}, title = {The view from the left}, journal = jfp, year = {2004}, pages = "69--111", volume = 14, number = 1, } @inproceedings{weirich-promotion, author = {Yorgey, Brent A and Weirich, Stephanie and Cretin, Julien and {Peyton Jones}, Simon and Vytiniotis, Dimitrios and Magalha\~{e}s, Jos\'{e} Pedro}, title = {Giving Haskell A Promotion}, booktitle = tldi12, year = 2012, url = {http://www.seas.upenn.edu/~sweirich/papers/tldi12.pdf}, } @Article{cervesato-llf, title = "A Linear Logical Framework", author = "Iliano Cervesato and Frank Pfenning", journal = ic, year = "2002", volume = "179", number = "1", pages = "19--75", } @InProceedings{watkins03types, author = "Keven Watkins and Iliano Cervesato and Frank Pfenning and David Walker", title = "A concurrent logical framework {I}: The propositional fragment", booktitle = types, volume = 3085, series = lncs, publisher = springer, year = "2003", } @InProceedings{DLG11, author = {Dal Lago, Ugo and Gaboardi, Marco}, title = "Linear Dependent Types and Relative Completeness", booktitle = lics11, pages = "133--142", year = {2011} } @InProceedings{KTDG12, title = "Superficially Substructural Types", author = "Krishnaswami, Neelakantan R. and Turon, Aaron and Dreyer, Derek and Garg, Deepak", booktitle = icfp12, year = 2012, } @misc{PalamidessiStronati12, title = {Differential privacy for relational algebra: Improving the sensitivity bounds via constraint systems}, author = {Palamidessi, Catuscia and Stronati, Marco}, note = {arXiv preprint arXiv:1207.0872}, year = {2012} } @inproceedings{CGL10, author = {Chaudhuri, Swarat and Gulwani, Sumit and Lublinerman, Roberto}, title = {Continuity analysis of programs}, booktitle = popl10, year = {2010}, pages = {57--70}, } @InProceedings{CGLN11, title = "Proving programs robust", author = "Swarat Chaudhuri and Sumit Gulwani and Roberto Lublinerman and Sara NavidPour", booktitle = { {ACM} {SIGSOFT} Symposium on the Foundations of Software Engineering ({FSE}), Szeged, Hungary }, year = "2011", ISBN = "978-1-4503-0443-6", pages = "102--112", URL = "http://doi.acm.org/10.1145/2025113.2025131", } @INPROCEEDINGS{Lowe-QIF02, author = {Gavin Lowe}, title = {Quantifying Information Flow}, booktitle = csfw02, year = {2002}, pages = {18--31} } @inproceedings{McCamantErnst08, author = {McCamant, Stephen and Ernst, Michael D.}, title = {Quantitative information flow as network flow capacity}, booktitle = pldi08, year = {2008}, isbn = {978-1-59593-860-2}, pages = {193--205}, } @inproceedings{AACP11, author = {Alvim, S., M{\'a}rio and Andres, E., Miguel and Chatzikokolakis, Konstantinos and Palamidessi, Catuscia}, title = {{On the relation between Differential Privacy and Quantitative Information Flow}}, booktitle = icalp11, year = {2011}, series = lncs, publisher = springer, volume = {6756}, pages = {60--76}, url = {http://hal.inria.fr/inria-00627937/en}, } @inproceedings{barthekoepf11, author = {Gilles Barthe and Boris K{\"o}pf}, title = {{Information-theoretic Bounds for Differentially Private Mechanisms}}, booktitle = csf11, publisher = ieee, pages = {191--204}, year = {2011} } @inproceedings{AgrawalSrikant00, title = {Privacy-preserving data mining}, author = {Agrawal, Rakesh and Srikant, Ramakrishnan}, booktitle = sigmod00, pages = {439--450}, year = {2000}, } @article{l-diversity, title = {l-diversity: Privacy beyond k-anonymity}, author = {Machanavajjhala, Ashwin and Kifer, Daniel and Gehrke, Johannes and Venkitasubramaniam, Muthuramakrishnan}, journal = {{ACM} Transactions on Knowledge Discovery from Data ({TKDD})}, volume = {1}, number = {1}, pages = {3}, year = {2007}, } @article{ESA04, title = {Privacy preserving mining of association rules}, author = {Evfimievski, Alexandre and Srikant, Ramakrishnan and Agrawal, Rakesh and Gehrke, Johannes}, journal = {Information Systems}, volume = {29}, number = {4}, pages = {343--364}, year = {2004}, publisher = elsevier } @inproceedings{GKSS08, title = {Composition attacks and auxiliary information in data privacy}, author = {Ganta, Srivatsava Ranjit and Kasiviswanathan, Shiva Prasad and Smith, Adam}, booktitle = kdd08, pages = {265--273}, year = {2008}, } @book{Hurwicz60, title = {Optimality and informational efficiency in resource allocation processes}, author = {Hurwicz, Leonid}, year = {1960}, publisher = {Stanford University Press} } @article{Vickrey61, title = {Counterspeculation, auctions, and competitive sealed tenders}, author = {Vickrey, William}, journal = {The Journal of Finance}, volume = {16}, number = {1}, pages = {8--37}, year = {1961}, } @article{Hurwicz72, title = {On informationally decentralized systems}, author = {Hurwicz, Leonid}, journal = {Decision and organization}, year = {1972}, publisher = {North-Holland Amsterdam} } @article{Myerson08, title = {Perspectives on mechanism design in economic theory}, author = {Myerson, Roger B}, journal = {The American Economic Review}, pages = {586--603}, year = {2008}, publisher = {JSTOR} } @incollection{BGBP-bigops08, title = {Canonical big operators}, author = {Bertot, Yves and Gonthier, Georges and Biha, Sidi Ould and Pasca, Ioana}, booktitle = tphol, pages = {86--101}, year = {2008}, publisher = springer } @techreport{Ramshaw79, title = {Formalizing the Analysis of Algorithms.}, author = {Ramshaw, Lyle Harold}, year = {1979}, institution = {Stanford University}, note = {STAN-CS-79-741} } @article{HartogVink02, title = {Verifying probabilistic programs using a {H}oare like logic}, author = {den Hartog, J I and de Vink, Erik P}, journal = {International Journal of Foundations of Computer Science}, volume = {13}, number = {03}, pages = {315--340}, year = {2002}, publisher = {World Scientific} } @article{Chadha07, title = {Reasoning about probabilistic sequential programs}, author = {Chadha, Rohit and Cruz-Filipe, Lu{\'\i}s and Mateus, Paulo and Sernadas, Am{\'\i}lcar}, journal = tcs, volume = {379}, number = {1}, pages = {142--165}, year = {2007}, publisher = elsevier } @misc{RandZdancewic15, author = {Rand, Robert and Zdancewic, Steve}, title = {A Formally Verified Probabilistic {H}oare Logic with Non-Termination}, year = 2015 } @article{Kozen81, title = {Semantics of probabilistic programs}, author = {Kozen, Dexter}, journal = {Journal of Computer and System Sciences}, volume = {22}, number = {3}, pages = {328--350}, year = {1981}, publisher = {Elsevier} } @article{HSP83, title = {Termination of probabilistic concurrent program}, author = {Hart, Sergiu and Sharir, Micha and Pnueli, Amir}, journal = toplas, volume = {5}, number = {3}, pages = {356--380}, year = {1983}, } @inproceedings{Hurd02, title = {A formal approach to probabilistic termination}, author = {Hurd, Joe}, booktitle = tphol, pages = {230--245}, year = {2002}, publisher = springer } @inproceedings{Chakarov-martingale, title = {Probabilistic program analysis with martingales}, author = {Chakarov, Aleksandar and Sankaranarayanan, Sriram}, booktitle = cav13, pages = {511--526}, year = {2013}, url = {https://www.cs.colorado.edu/~srirams/papers/cav2013-martingales.pdf} } @inproceedings{FerrerHermanns15, title = {Probabilistic Termination: Soundness, Completeness, and Compositionality}, author = {Ferrer Fioriti, Luis Mar{\'\i}a and Hermanns, Holger}, booktitle = popl15, pages = {489--501}, year = {2015}, url = {http://www.ae-info.org/attach/User/Hermanns_Holger/Publications/FH-POPL15.pdf}, } @inproceedings{Kozen06, title = {Coinductive Proof Principles for Stochastic Processes}, author = {Kozen, Dexter}, booktitle = lics06, pages = {359--366}, year = {2006}, organization = ieee } @inproceedings{liquid-haskell, title = {Abstract refinement types}, author = {Vazou, Niki and Rondon, Patrick M and Jhala, Ranjit}, booktitle = esop13, pages = {209--228}, year = {2013}, publisher = springer } @inproceedings{liquid-ml, title = {Liquid types}, author = {Rondon, Patrick M and Kawaguci, Ming and Jhala, Ranjit}, booktitle = pldi08, volume = {43}, number = {6}, pages = {159--169}, year = {2008}, } @book{Thorisson00, author = {Hermann Thorisson}, title = {Coupling, Stationarity, and Regeneration}, publisher = springer, year = {2000} } @book{Lindvall02, title = {Lectures on the coupling method}, author = {Lindvall, Torgny}, year = {2002}, publisher = {Courier Corporation} } @book{Villani08, title = {Optimal transport: old and new}, author = {Villani, C{\'e}dric}, year = {2008}, publisher = springer } @techreport{DengD11, Author = {Deng, Yuxin and Du, Wenjie}, Institution = {Carnegie Mellon University}, Month = {March}, Number = {CMU-CS-11-110}, Title = {Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation}, Year = {2011}, url = {http://arxiv.org/abs/1103.4577} } @article{Yang07, author = {H. Yang}, title = {Relational separation logic}, journal = tcs, volume = 375, number = {1--3}, year = 2007, pages = {308--334}, url = {http://www.cs.ox.ac.uk/people/hongseok.yang/paper/data.pdf} } @article{mufa1994optimal, title = {Optimal Markovian couplings and applications}, author = {Mufa, Chen}, journal = {Acta Mathematica Sinica}, volume = {10}, number = {3}, pages = {260--275}, year = {1994}, publisher = springer } @article{mount1974informational, title={The informational size of message spaces}, author={Mount, Kenneth and Reiter, Stanley}, journal=jet, volume={8}, number={2}, pages={161--192}, year={1974}, url={http://www.kellogg.northwestern.edu/faculty/reiter/papers/22_informationalsize.pdf}, publisher={Elsevier} } @inproceedings{devanur2011prior, title={Prior-independent multi-parameter mechanism design}, author={Devanur, Nikhil and Hartline, Jason and Karlin, Anna and Nguyen, Thach}, booktitle=wine11, pages={122--133}, year={2011}, publisher=springer, url={http://users.eecs.northwestern.edu/~hartline/papers/auctions-WINE-11.pdf}, } @inproceedings{CR14, author = {Cole, Richard and Roughgarden, Tim}, title = {The Sample Complexity of Revenue Maximization}, booktitle = stoc14, year = {2014}, pages = {243--252}, numpages = {10}, url={http://arxiv.org/abs/1502.00963}, keywords = {Myerson's auction, sample complexity}, } @inproceedings{blum2005near, author = {Blum, Avrim and Hartline, Jason D}, booktitle = soda05, pages = {1156--1163}, publisher = siam, title = {Near-optimal online auctions}, url={http://users.eecs.northwestern.edu/~hartline/papers/online-auctions-SODA-05.pdf}, year = 2005 } @inproceedings{balcan2005mechanism, author = {Balcan, Maria{-}Florina and Blum, Avrim and Hartline, Jason D and Mansour, Yishay}, title = {Mechanism Design via Machine Learning}, booktitle = focs05, pages = {605--614}, url = {http://users.eecs.northwestern.edu/~hartline/papers/auctions-FOCS-05.pdf}, year = 2005, } @INPROCEEDINGS {B+03, author = {Blum, Avrim and Kumar, Vijay and Rudra, Atri and Wu, Felix}, title = "Online Learning in Online Auctions", booktitle = soda03, url = {http://www.cs.cmu.edu/~avrim/Papers/onlineauction.pdf}, year = 2003, } @inproceedings{CGMsoda13, author = {Cesa-Bianchi, Nicolò and Gentile, Claudio and Mansour, Yishay}, booktitle = soda13, pages = {1190--1204}, publisher = siam, title = {Regret Minimization for Reserve Prices in Second-Price Auctions}, url = {http://epubs.siam.org/doi/pdf/10.1137/1.9781611973105.86}, year = 2013 } @inproceedings{hartline2009simple, author = {Hartline, Jason D and Roughgarden, Tim}, booktitle = ec09, title = {Simple versus optimal mechanisms}, year = 2009, url = {http://www.sigecom.org/exchanges/volume_8/1/hartline.pdf}, } @Inproceedings {BBDSics11, author = {Babaioff, Moshe and Blumrosen, Liad and Dughmi, Shaddin and Singer, Yaron}, booktitle = itcs11, publisher = {Tsinghua University Press}, title = {Posting Prices with Unknown Distributions}, year = {2011}, url = {http://research.microsoft.com/apps/pubs/default.aspx?id=144123}, } @inproceedings {morgenstern15pseudo, author = {Jamie Morgenstern and Tim Roughgarden}, title = {The Pseudo-Dimension of Nearly-Optimal Auctions}, booktitle = nips15, year = 2015, url = {http://arxiv.org/abs/1506.03684}, } @unpublished{RS15, author = "Roughgarden, Tim and Schrijvers, Okke", title = "Ironing in the Dark", note = "Under submission", year = 2015 } @inproceedings{rubensteinsubadditive, author = {Rubinstein, Aviad and Weinberg, S. Matthew}, title = {Simple Mechanisms for a Subadditive Buyer and Applications to Revenue Monotonicity}, booktitle = ec15, year = {2015}, pages = {377--394}, url = {http://people.csail.mit.edu/smweinberg/ec15subadditive.pdf}, } @inproceedings{balcan2014learning, title={Learning economic parameters from revealed preferences}, author={Balcan, Maria-Florina and Daniely, Amit and Mehta, Ruta and Urner, Ruth and Vazirani, Vijay V}, booktitle=wine14, pages={338--353}, year={2014}, publisher=springer, url={http://arxiv.org/abs/1407.7937} } @inproceedings{dughmi2014sampling, year={2014}, booktitle=wine14, volume={8877}, series=lncs, title={Sampling and Representation Complexity of Revenue Maximization}, publisher=springer, author={Dughmi, Shaddin and Han, Li and Nisan, Noam}, pages={277--291}, url={http://arxiv.org/abs/1402.4535}, } @inproceedings{babaioffadditive, Author = {Babaioff, Moshe and Immorlica, Nicole and Lucier, Brendan and Weinberg, S. Matthew}, Booktitle = focs14, Title = {A Simple and Approximately Optimal Mechanism for an Additive Buyer}, Year = {2014}, url = {http://arxiv.org/abs/1405.6146} } @inproceedings{yao2015soda, author = {Yao, Andrew Chi-Chih}, title = {An $n$-to-$1$ Bidder Reduction for Multi-item Auctions and its Applications}, booktitle = soda14, chapter = {8}, year={2015}, pages = {92--109}, url = {http://arxiv.org/abs/1406.3278} } @inproceedings{huang2014making, author = {Huang, Zhiyi and Mansour, Yishay and Roughgarden, Tim}, title = {Making the Most of Your Samples}, booktitle = ec15, year = {2015}, isbn = {978-1-4503-3410-5}, pages = {45--60}, keywords = {auction, revenue, sample complexity}, url = {http://arxiv.org/abs/1407.2479}, } @article{dhangwatnotai2014revenue, title={Revenue maximization with a single sample}, author={Dhangwatnotai, Peerapong and Roughgarden, Tim and Yan, Qiqi}, journal=geb, year={2014}, publisher={Elsevier}, url={http://theory.stanford.edu/~tim/papers/single.pdf}, } @inproceedings{chawla2007algorithmic, author = {Chawla, Shuchi and Hartline, Jason and Kleinberg, Robert}, title = {Algorithmic Pricing via Virtual Valuations}, booktitle = ec07, year = {2007}, pages = {243--251}, url = {http://arxiv.org/abs/0808.1671}, } @article{GS99a, title = "The {E}nglish Auction with Differentiated Commodities", journal = jet, volume = "92", number = "1", pages = "66--95", year = "2000", issn = "0022-0531", url = "http://www.sciencedirect.com/science/article/pii/S0022053199925802", author = "Faruk Gul and Ennio Stacchetti" } @Article{OL15, author={Ostrovsky, Michael and Paes Leme, Renato}, title={Gross substitutes and endowed assignment valuations}, journal={Theoretical Economics}, year=2015, volume={10}, number={3}, pages={853--865}, url={https://econtheory.org/ojs/index.php/te/article/viewFile/20150853/13867/412} } @inproceedings{Mur96, year={1996}, isbn={978-3-540-61310-7}, booktitle=ipco06, volume={1084}, series=lncs, title={Convexity and {S}teinitz's exchange property}, url={http://dx.doi.org/10.1007/3-540-61310-2_20}, publisher=springer, author={Murota, Kazuo}, pages={260--274}, } @article{MS99, author = {Murota, Kazuo and Shioura, Akiyoshi}, title = {{M}-{C}onvex Function on Generalized Polymatroid}, journal = {Mathematics of Operations Research}, volume = {24}, number = {1}, pages = {95--105}, year = {1999}, URL = {http://dx.doi.org/10.1287/moor.24.1.95}, eprint = {http://dx.doi.org/10.1287/moor.24.1.95}, } @article{FY03, author = {Fujishige, Satoru and Yang, Zaifu}, title = {A Note on {K}elso and {C}rawford's {G}ross {S}ubstitutes Condition}, journal = {Mathematics of Operations Research}, volume = {28}, number = {3}, pages = {463--469}, year = {2003}, URL = {http://dx.doi.org/10.1287/moor.28.3.463.16393}, eprint = {http://dx.doi.org/10.1287/moor.28.3.463.16393}, } @article{MT10, title = "Characterization of the {W}alrasian equilibria of the assignment model ", journal = "Journal of Mathematical Economics", volume = "46", number = "1", pages = "6--20", year = "2010", issn = "0304-4068", url = "http://www.sciencedirect.com/science/article/pii/S0304406809000627", author = "Debasis Mishra and Dolf Talman", } @book{shalev2014book, title={Understanding Machine Learning: From Theory to Algorithms}, author={Shalev-Shwartz, Shai and Ben-David, Shai}, year=2014, publisher=cup } @article{BLN13, author = {Ben-Zwi, Oren and Lavi, Ron and Newman, Ilan}, title = {Ascending auctions and Walrasian equilibrium}, journal = {CoRR}, volume = {abs/1301.1153}, year = {2013}, url = {http://arxiv.org/abs/1301.1153}, } @article{ehrenfeucht1989general, title={A general lower bound on the number of examples needed for learning}, author={Ehrenfeucht, Andrzej and Haussler, David and Kearns, Michael and Valiant, Leslie}, journal={Information and Computation}, volume={82}, number={3}, pages={247--261}, year={1989}, url={https://www.cis.upenn.edu/~mkearns/papers/lower.pdf}, publisher={Elsevier}, } @book{vapnik1982estimation, title={Estimation of dependences based on empirical data}, author={Vapnik, Vladimir Naumovich and Kotz, Samuel}, year={1982}, publisher=springer, } @inproceedings{daniely2014multiclass, title={Optimal learners for multiclass problems}, author={Daniely, Amit and Shalev-Shwartz, Shai}, booktitle=colt14, pages={287--316}, url={http://arxiv.org/abs/1405.2420}, year={2014} } @techreport{littlestone1986compression, title={Relating data compression and learnability}, author={Littlestone, Nick and Warmuth, Manfred}, year={1986}, url={https://users.soe.ucsc.edu/~manfred/pubs/lrnk-olivier.pdf}, institution={University of California, Santa Cruz} } @article{murota1996valuated, title={Valuated matroid intersection {I}: Optimality criteria}, author={Murota, Kazuo}, journal={{SIAM} Journal on Discrete Mathematics}, volume={9}, number={4}, pages={545--561}, year={1996}, url={http://www.keisu.t.u-tokyo.ac.jp/research/techrep/data/2003/METR03-42.pdf}, } @article{ST15, author = {Shioura, Akiyoshi and Tamura, Akihisa}, title = {Gross Substitutes Condition and Discrete Concavity for Multi-Unit Valuations: a Survey}, journal = {Journal of the Operations Research Society of Japan}, volume = {58}, number = {1}, year = 2015, pages = {61--103}, url = {http://www.orsj.or.jp/~archive/pdf/e_mag/Vol.58_01_061.pdf} } @Book{Matroid, Title = {Matroid Theory}, Author = {Oxley, James G}, Publisher = {Oxford University Press}, Year = {1997}, Series = {Oxford Graduate Texts in Mathematics}, } @inproceedings{elkind2007, title={Designing and learning optimal finite support auctions}, author={Elkind, Edith}, booktitle=ec07, pages={736--745}, year={2007}, url={http://eprints.soton.ac.uk/263443/1/finsup.pdf} } @inproceedings{medina2014learning, title={Learning Theory and Algorithms for revenue optimization in second price auctions with reserve}, author={Medina, Andres Munoz and Mohri, Mehryar}, booktitle=icml14, pages={262--270}, year={2014}, url={http://arxiv.org/abs/1310.5665} } @article{arrow1954existence, title={Existence of an equilibrium for a competitive economy}, author={Arrow, Kenneth J and Debreu, Gerard}, journal={Econometrica}, pages={265--290}, year={1954}, url={http://web.stanford.edu/class/msande311/arrow-debreu.pdf} } @inproceedings{deng02complexity, author = {Deng, Xiaotie and Papadimitriou, Christos and Safra, Shmuel}, title = {On the Complexity of Equilibria}, booktitle = stoc02, year = {2002}, isbn = {1-58113-495-9}, pages = {67--71}, numpages = {5}, acmid = {509920}, url={http://dl.acm.org/citation.cfm?id=509920} } @article{nisan06communication, Author = {Nisan, Noam and Segal, Ilya}, Issn = {0022-0531}, Journal = jet, Keywords = {Distributional complexity}, Number = {1}, Pages = {192--224}, Title = {The communication requirements of efficient allocations and supporting prices}, Volume = {129}, Year = {2006}, url={http://web.stanford.edu/~isegal/prices.pdf} } @inproceedings{DH09, title={The {A}dwords problem: {O}nline keyword matching with budgeted bidders under random permutations}, author={Devanur, Nikhil R and Hayes, Thomas P}, booktitle=ec09, pages={71--78}, year={2009}, url={http://research.microsoft.com/en-us/um/people/nikdev/pubs/adwords.pdf} } @techreport{samplingbalcan07, title = {Random Sampling Auctions for Limited Supply}, author = {Balcan, Maria-Florina and Devanur, Nikhil and Hartline, Jason D and Talwar, Kunal}, url = {http://reports-archive.adm.cs.cmu.edu/anon/2007/CMU-CS-07-154.pdf}, year = {2007}, institution = {Carnegie Mellon University}, Date-Added = {09-01-2007}, } @article{hanneke15, author = {Hanneke, Steve}, title = {The Optimal Sample Complexity of {PAC} Learning}, journal = {CoRR}, volume = {abs/1507.00473}, year = {2015}, url = {http://arxiv.org/abs/1507.00473}, timestamp = {Sun, 02 Aug 2015 18:42:02 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/Hanneke15}, bibsource = {dblp computer science bibliography, http://dblp.org} } @book{pollard1984, title= "Convergence of stochastic processes", author={Pollard, David}, year={1984}, publisher={David Pollard}, url = {http://www.stat.yale.edu/~pollard/Books/1984book/pollard1984.pdf}, } @article{VC, title={On the uniform convergence of relative frequencies of events to their probabilities}, author={Vapnik, Vladimir N and Chervonenkis, A Ya}, journal={Theory of Probability \& Its Applications}, volume={16}, number={2}, pages={264--280}, year={1971}, url={http://www.springer.com/cda/content/document/cda_downloaddocument/9783642411359-c1.pdf?SGWID=0-0-45-1431218-p175483535}, publisher=siam } @book{AB, author = "Anthony, Martin and Bartlett, Peter L", title = {Neural Network Learning: Theoretical Foundations}, year = {1999}, publisher = cup, } @inproceedings{DNRR15, year={2015}, isbn={978-3-662-48799-0}, booktitle=ascrypt15, title={Pure Differential Privacy for Rectangle Queries via Private Partitions}, url={http://dx.doi.org/10.1007/978-3-662-48800-3_30}, publisher=springer, author={Dwork, Cynthia and Naor, Moni and Reingold, Omer and Rothblum, Guy N}, pages={735--751}, } @inproceedings{BartheO13, author = {Barthe, Gilles and Olmedo, Federico}, title = {Beyond Differential Privacy: Composition Theorems and Relational Logic for $f$-divergences between Probabilistic Programs}, booktitle = icalp13, series = lncs, volume = {7966}, pages = {49--60}, publisher = springer, year = {2013}, url = {http://certicrypt.gforge.inria.fr/2013.ICALP.pdf} } @InProceedings{conf/popl/EbadiSS15, title = "Differential Privacy: Now it's Getting Personal", author = "Hamid Ebadi and David Sands and Gerardo Schneider", booktitle = popl15, year = "2015", ISBN = "978-1-4503-3300-9", pages = "69--81", URL = "http://dl.acm.org/citation.cfm?id=2676726", } @inproceedings{DBLP:conf/stoc/DworkFHPRR15, author = {Dwork, Cynthia and Feldman, Vitaly and Hardt, Moritz and Pitassi, Toniann and Reingold, Omer and Roth, Aaron}, title = {Preserving Statistical Validity in Adaptive Data Analysis}, booktitle = stoc15, pages = {117--126}, year = {2015}, url = {http://doi.acm.org/10.1145/2746539.2746580}, } @inproceedings{xu:hal-00879140, TITLE = {Metrics for Differential Privacy in Concurrent Systems}, AUTHOR = {Xu, Lili and Chatzikokolakis, Konstantinos and Lin, Huimin}, URL = {https://hal.inria.fr/hal-00879140}, BOOKTITLE = {IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE), Berlin, Germany}, EDITOR = {Erika Abraham and Catuscia Palamidessi}, PUBLISHER = springer, SERIES = lncs, VOLUME = {8461}, PAGES = {199--215}, YEAR = {2014}, MONTH = Jun, KEYWORDS = {differential privacy ; probabilistic automata ; bisimulation metrics ; verification}, PDF = {https://hal.inria.fr/hal-00879140/file/forte-hal.pdf}, HAL_ID = {hal-00879140}, HAL_VERSION = {v2}, } @inproceedings{Kozen79, Author = {Kozen, Dexter}, Booktitle = focs79, Pages = {101--114}, Title = {Semantics of probabilistic programs}, Year = {1979}} @InProceedings{ChakarovS14, author = {Aleksandar Chakarov and Sriram Sankaranarayanan}, title = {Expectation Invariants as Fixed Points of Probabilistic Programs}, year = {2014}, pages = {85--100}, publisher = springer, booktitle = sas14, series = lncs, volume = {8723}, url = {https://www.cs.colorado.edu/~srirams/papers/sas14-expectations.pdf} } @inproceedings{CousotM12, author = {Patrick Cousot and Michael Monerau}, title = {Probabilistic Abstract Interpretation}, booktitle = esop12, series = lncs, volume = {7211}, pages = {169--193}, publisher = springer, year = {2012}, url = {http://www.di.ens.fr/~cousot/publications.www/Cousot-Monerau-ESOP2012-extended.pdf} } @incollection{dwork2006our, title={Our data, ourselves: Privacy via distributed noise generation}, author={Dwork, Cynthia and Kenthapadi, Krishnaram and McSherry, Frank and Mironov, Ilya and Naor, Moni}, booktitle=eucrypt06, pages={486--503}, year={2006}, publisher=springer } @inproceedings{lyu2016understanding, title={Understanding the Sparse Vector Technique for Differential Privacy}, author={Lyu, Min and Su, Dong and Li, Ninghui}, booktitle=vldb17, volume=10, number=6, pages={637--648}, url={http://arxiv.org/abs/1603.01699}, year={2017}, } @inproceedings{DBLP:journals/corr/OhV13, author = { Peter Kairouz and Sewoong Oh and Pramod Viswanath}, title = {The Composition Theorem for Differential Privacy}, booktitle = icml15, volume = {https://arxiv.org/abs/1311.0776}, year = {2015}, publisher = jmlr } @article{dwork2015reusable, title={The reusable holdout: Preserving validity in adaptive data analysis}, author={Dwork, Cynthia and Feldman, Vitaly and Hardt, Moritz and Pitassi, Toniann and Reingold, Omer and Roth, Aaron}, journal={Science}, volume={349}, number={6248}, pages={636--638}, year={2015}, publisher={American Association for the Advancement of Science} } @article{aldous93shift, author = {Aldous, D. J. and Thorisson, H.}, citeulike-article-id = {4046853}, journal = {Stochastic Proc. Appl}, keywords = {aldousbib}, mrnumber = {1198659}, pages = {1--14}, posted-at = {2009-02-13 21:55:05}, priority = {2}, title = {{Shift-Coupling}}, volume = {44}, year = {1993} } @inproceedings{bubley1997path, title={Path coupling: A technique for proving rapid mixing in {M}arkov chains}, author={Bubley, Russ and Dyer, Martin}, booktitle=focs97, pages={223--231}, year={1997}, } @unpublished{BunS2016, author = {{Bun}, M. and {Steinke}, T.}, title = "{Concentrated Differential Privacy: Simplifications, Extensions, and Lower Bounds}", journal = {ArXiv e-prints}, archivePrefix = "arXiv", eprint = {1605.02065}, primaryClass = "cs.CR", keywords = {Computer Science - Cryptography and Security, Computer Science - Data Structures and Algorithms, Computer Science - Information Theory, Computer Science - Learning}, year = 2016, } @inproceedings{BunSU16, author = {Bun, Mark and Steinke, Thomas and Ullman, Jonathan}, title = {Make Up Your Mind: The Price of Online Queries in Differential Privacy}, booktitle = soda17, year = 2017, url = {https://arxiv.org/abs/1604.04618} } @inproceedings{moser2009constructive, title={A constructive proof of the {Lov{\'a}sz Local Lemma}}, author={Moser, Robin A}, booktitle=stoc09, pages={343--350}, year={2009}, } @inproceedings{micciancio1997oblivious, title={Oblivious data structures: applications to cryptography}, author={Micciancio, Daniele}, booktitle=stoc97, pages={456--464}, year={1997}, } @inproceedings{jonsson1991specification, title={Specification and refinement of probabilistic processes}, author={Jonsson, Bengt and Larsen, Kim Guldstrand}, booktitle=lics91, pages={266--277}, year={1991}, } @inproceedings{rogers2016privacy, title={Privacy odometers and filters: Pay-as-you-go composition}, author={Rogers, Ryan and Vadhan, Salil and Roth, Aaron and Ullman, Jonathan}, booktitle=nips16, pages={1921--1929}, year={2016}, url={http://arxiv.org/abs/1605.08294} } @inproceedings{sousa2016cartesian, title={Cartesian {H}oare logic for verifying $k$-safety properties}, author={Sousa, Marcelo and Dillig, Isil}, booktitle=pldi16, pages={57--69}, year={2016}, } @inproceedings{BKOZ12-popl, title={Probabilistic relational reasoning for differential privacy}, author={Barthe, Gilles and K{\"o}pf, Boris and Olmedo, Federico and Zanella B{\'e}guelin, Santiago}, booktitle=popl12, volume={47}, number={1}, pages={97--110}, year={2012}, } @inproceedings{zhang2016autopriv, author = {Zhang, Danfeng and Kifer, Daniel}, title = {{LightDP}: Towards Automating Differential Privacy Proofs}, booktitle = popl17, year = {2017}, pages = {888--901}, url = {https://arxiv.org/abs/1607.08228}, } @article{JerrumS89, author = {Mark Jerrum and Alistair Sinclair}, title = {Approximating the Permanent}, journal = siamjc, volume = {18}, number = {6}, pages = {1149--1178}, year = {1989}, url = {http://dx.doi.org/10.1137/0218077}, doi = {10.1137/0218077}, timestamp = {Mon, 12 Sep 2011 16:10:07 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/journals/siamcomp/JerrumS89}, bibsource = {dblp computer science bibliography, http://dblp.org} } @article{DBLP:journals/rsa/Jerrum95, author = {Mark Jerrum}, title = {A Very Simple Algorithm for Estimating the Number of $k$-Colorings of a Low-Degree Graph}, journal = {Random Struct. Algorithms}, volume = {7}, number = {2}, pages = {157--166}, year = {1995}, url = {http://dx.doi.org/10.1002/rsa.3240070205}, doi = {10.1002/rsa.3240070205}, timestamp = {Sat, 14 Apr 2012 16:35:21 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/journals/rsa/Jerrum95}, bibsource = {dblp computer science bibliography, http://dblp.org} } @inproceedings{Sato16, title = {Approximate Relational {H}oare Logic for Continuous Random Samplings}, author = {Tetsuya Sato}, booktitle = mfps16, pages = {277--298}, year = 2016, volume = 325, url = {https://arxiv.org/abs/1603.01445}, series = entcs, publisher = elsevier } @article{strassen1965existence, title={The existence of probability measures with given marginals}, author={Strassen, Volker}, journal={The Annals of Mathematical Statistics}, pages={423--439}, year={1965}, publisher={Institute of Mathematical Statistics}, url={http://projecteuclid.org/euclid.aoms/1177700153} } @inproceedings{tracolDZ11, author = {Mathieu Tracol and Jos\'{e}e Desharnais and Abir Zhioua}, title = {Computing Distances between Probabilistic Automata}, booktitle = {Workshop on Quantitative Aspects of Programming Languages ({QAPL}), Saarbr{\"{u}}cken, Germany}, pages = {148--162}, year = {2011}, url = {http://dx.doi.org/10.4204/EPTCS.57.11}, doi = {10.4204/EPTCS.57.11}, timestamp = {Mon, 28 Oct 2013 16:56:55 +0100}, biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1107-1206}, bibsource = {dblp computer science bibliography, http://dblp.org} } @inproceedings{desharnaisLT08, author = {Jos\'{e}e Desharnais and Fran\c{c}ois Laviolette and Mathieu Tracol}, booktitle={International Conference on Quantitative Evaluation of Systems ({QEST}), Saint Malo, France}, title={Approximate Analysis of Probabilistic Processes: Logic, Simulation and Games}, year={2008}, pages={264--273}, doi={10.1109/QEST.2008.42}, month=sep} @inproceedings{LarsenS89, author = {Larsen, Kim Guldstrand and Skou, Arne}, title = {Bisimulation Through Probabilistic Testing}, booktitle = popl89, pages = {344--352}, year = {1989}, url = {http://doi.acm.org/10.1145/75277.75307}, timestamp = {Mon, 21 May 2012 16:19:51 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/LarsenS89}, bibsource = {dblp computer science bibliography, http://dblp.org} } @inproceedings{giacalone1990algebraic, title={Algebraic reasoning for probabilistic concurrent systems}, author={Giacalone, Alessandro and Jou, Chi-Chang and Smolka, Scott A}, booktitle={{IFIP} {TC2} Working Conference on Programming Concepts and Methods}, year={1990}, } @inproceedings{SegalaTurrini07, author={R. Segala and A. Turrini}, booktitle=csf07, title={Approximated Computationally Bounded Simulation Relations for Probabilistic Automata}, year={2007}, pages={140--156}, doi={10.1109/CSF.2007.8}, ISSN={1063-6900}, month=jul } @phdthesis{OlmedoThesis, title = {Approximate Relational Reasoning for Probabilistic Programs}, author = {Federico Olmedo}, school = {Universidad Polit\'ecnica de Madrid}, year = {2014}, url = {http://software.imdea.org/~federico/thesis.pdf} }