%%%%%%%%%%%%%%%%%%%%%%%%%%%% UNPUBLISHED %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @unpublished{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}, year = 2016, jh = yes, eprint = yes, url = {http://arxiv.org/abs/1602.05681}, } @unpublished{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}, year = 2016, jh = yes, docs = yes, } @unpublished{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}, year = 2016, url = {http://arxiv.org/abs/1601.05047}, jh = yes, eprint = yes, } @unpublished{HKM-verif15, 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}, year = {2015}, url = {http://arxiv.org/abs/1502.04052}, jh = yes, eprint = yes } @unpublished{BEGGHS15, 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 = 2015, jh = yes, docs = yes } %%%%%%%%%%%%%%%%%%%%%%%%%%%% CONFERENCES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @inproceedings{HMRRV16, title = {Do prices coordinate markets?}, author = {Hsu, Justin and Morgenstern, Jamie and Rogers, Ryan and Roth, Aaron and Vohra, Rakesh}, booktitle = stoc16, year = 2016, url = {http://arxiv.org/abs/1511.00925}, jh = yes, eprint = yes, note = {To appear.} } @inproceedings{HHRW16, author = {Hsu, Justin and Huang, Zhiyi and Roth, Aaron and Wu, Zhiwei Steven}, title = {Jointly private convex programming}, booktitle = soda16, year = {2016}, url = {http://arxiv.org/abs/1411.0998}, jh = yes, eprint = yes, slides = yes, } @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, year = 2015, jh = yes, slides = yes, eprint = yes, volume = {9450}, pages = {387--401}, url = {http://arxiv.org/abs/1509.03476}, } @inproceedings{AHJ15, title = {Online assignment with heterogeneous tasks in crowdsourcing markets}, author = {Assadi, Sepehr and Hsu, Justin and Jabbari, Shahin}, year = {2015}, booktitle = hcomp15, url = {http://arxiv.org/abs/1508.03593}, jh = yes, eprint = yes, } @inproceedings{HsuTaxes, author = {Justin Hsu}, title = {Death, taxes, and formal verification (Abstract)}, year = {2015}, booktitle = snapl15, jh = yes, slides = yes, docs = yes } @inproceedings{GHaccuracy, author = {Marco Gaboardi and Justin Hsu}, title = {A Theory {AB} toolbox}, year = {2015}, booktitle = snapl15, jh = yes, slides = yes, docs = yes } @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, year = {2015}, url = {http://arxiv.org/abs/1407.6845}, jh = yes, slides = yes, eprint = yes } @inproceedings{AGGH14, author = {de Amorim, Arthur Azevedo and Gaboardi, Marco and Gallego Arias, Emilio Jes{\'u}s and Hsu, Justin}, title = {Really naturally linear indexed type-checking}, booktitle = {Symposium on Implementation and Application of Functional Programming Languages (IFL), Boston, Massachusetts}, year = {2014}, url = {http://arxiv.org/abs/1503.04522}, jh = yes, slides = yes, eprint = yes } @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, year = {2014}, url = {http://arxiv.org/abs/1407.2988}, jh = yes, eprint = yes } @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, year = 2014, url = {http://arxiv.org/abs/1402.3329}, jh = yes, slides = yes, eprint = yes } @inproceedings{HRRU14, author = {Hsu, Justin and Roth, Aaron and Roughgarden, Tim and Ullman, Jonathan}, title = {Privately solving linear programs}, booktitle = icalp14, year = {2014}, pages = {612--624}, url = {http://arxiv.org/abs/1402.3631}, timestamp = {Fri, 31 Oct 2014 14:45:31 +0100}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/icalp/HsuRRU14}, bibsource = {dblp computer science bibliography, http://dblp.org}, jh = yes, slides = yes, eprint = yes } @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, year = {2014}, url = {http://arxiv.org/abs/1402.1526}, jh = yes, slides = yes, poster = yes, eprint = yes } @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}, 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 = yes, eprint = yes } @inproceedings{WHE13, title = {Towards dependently typed {H}askell: {S}ystem {FC} with kind equality}, author = {Weirich, Stephanie and Hsu, Justin and Eisenberg, Richard A}, booktitle = icfp13, url = {http://www.cis.upenn.edu/~justhsu/docs/nokinds.pdf}, volume = {13}, year = {2013}, jh = yes, docs = yes } @inproceedings{HRU13, title = {Differential privacy for the analyst via private equilibrium computation}, author = {Hsu, Justin and Roth, Aaron and Ullman, Jonathon}, url = {http://arxiv.org/abs/1211.0877}, booktitle = stoc13, pages = {341--350}, year = {2013}, jh = yes, slides = yes, eprint = yes } @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 } @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, docs = yes } @inproceedings{HKR12, title = {Distributed private heavy hitters}, author = {Hsu, Justin and Khanna, Sanjeev and Roth, Aaron}, booktitle = icalp12, pages = {461--472}, 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, slides = yes, eprint = yes } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% JOURNALS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @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 M 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}, month = oct, 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{certipriv, 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}, publisher = {SIAM} } @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}, } @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}, organization = {ACM} } @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}, publisher = {SIAM}, 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 = {Cambridge University Press} } @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} } @techreport{CKRW14, title = {Privacy and Truthful Equilibrium Selection for Aggregative Games}, author = {Cummings, Rachel and Kearns, Michael and Roth, Aaron and Wu, Zhiwei Steven}, year = {2014}, url = {http://arxiv.org/abs/1407.7740} } @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}, Publisher = {ACM}, 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, address = {Heidelberg}, series = lncs, volume = {3148}, year = {2004}, url = {http://software.imdea.org/~ab/Publications/ifalftr.pdf} } @inproceedings{BartheGZ09, Address = {New York}, 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, address = {Heidelberg}, series = lncs, volume = {5014}, year = {2008}, url = {http://llvm.org/pubs/2008-05-CoVaC.pdf} } @inproceedings{TerauchiA05, Address = {Heidelberg}, 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, title = {Calibrating noise to sensitivity in private data analysis}, author = {Cynthia Dwork and Frank McSherry and Kobbi Nissim and Adam Smith}, pages = {265--284}, url = {http://dx.doi.org/10.1007/11681878_14}, booktitle = tcc06, year = {2006} } @article{Tschantz201161, title = {Formal Verification of Differential Privacy for Interactive Systems (Extended Abstract)}, author = {Tschantz, Michael Carl and Kaynar, Dilsun and Datta, Anupam}, journal = entcs, volume = "276", number = "0", pages = {61--79}, year = "2011", issn = "1571--0661", url = {http://arxiv.org/pdf/1101.2819v1} } @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 (CSUR)}, volume = {28}, number = {2}, pages = {324--328}, year = {1996}, url = {http://dl.acm.org/citation.cfm?id=234740}, publisher = {ACM} } @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 = {Cambridge University Press}, address = {New York, NY, USA}, } @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", publisher = {ACM} } @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}, publisher = {ACM} } @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}, editor = {Alessandro Aldini and Javier Lopez and Fabio Martinelli}, 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{Hoare69, author = {C. A. R. Hoare}, title = {An Axiomatic Basis for Computer Programming}, journal = cacm, year = {1969}, volume = {12}, number = {10} } @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, Publisher = {IEEE}, 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}, organization = {ACM} } @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}, publisher = {SIAM} } @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}, organization = {SIAM} } @inproceedings{BH11, title = {Bayesian incentive compatibility via fractional assignments}, author = {Bei, Xiaohui and Huang, Zhiyi}, booktitle = soda11, pages = {720--733}, year = {2011}, organization = {SIAM} } @book{Rou05, title = {Selfish routing and the price of anarchy}, author = {Roughgarden, Tim}, volume = {174}, year = {2005}, publisher = mitpress } @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} } @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 Berlin Heidelberg}, author = {Tadjouddine, Emmanuel M. and Guerin, Frank and Vasconcelos, Wamberto}, pages = {197-214}, language = {English} } @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", month = sep, 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, address = {Heidelberg}, 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, month = nov, 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}, address = {New York, NY, USA}, } @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}, publisher = {ACM} } @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 Hoare 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 Hoare 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}, organization = {ACM} } @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 Science} } @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}, address={Singapore} } @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, publisher = {ACM}, 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, publisher = {ACM}, 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, month = {January}, 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, pages = "To Appear", 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}, numpages = {18}, acmid = {2764510}, publisher = {ACM}, 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={Lecture Notes in Computer Science}, 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}, publisher = {ACM}, 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}, numpages = {16}, acmid = {2764475}, publisher = {ACM}, 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}, numpages = {9}, acmid = {1250946}, publisher = {ACM}, 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}, month=sep, keywords={Substitutability; matching; combinatorial auctions; matroids}, abstract={We show that the class of preferences satisfying the Gross Substitutes condition of Kelso and Crawford (1982) is strictly larger than the class of Endowed Assignment Valuations of Hatfield and Milgrom (2005), thus resolving the open question posed by the latter paper. In particular, our result implies that not every substitutable valuation function can be \"decomposed\" into a combination of unit-demand valuations.}, 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={Lecture Notes in Computer Science}, editor={Cunningham, William H and McCormick, S Thomas and Queyranne, Maurice}, title={Convexity and {S}teinitz's exchange property}, url={http://dx.doi.org/10.1007/3-540-61310-2_20}, publisher={Springer Berlin Heidelberg}, author={Murota, Kazuo}, pages={260--274}, language={English} } @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}, abstract = { The concept of M-convex function, introduced by Murota (1996), is a quantitative generalization of the set of integral points in an integral base polyhedron as well as an extension of valuated matroid of Dress and Wenzel (1990). In this paper, we extend this concept to functions on generalized polymatroids with a view to providing a unified framework for efficiently solvable nonlinear discrete optimization problems. } } @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}, abstract = { In their 1982 article, Kelso and Crawford proposed a gross substitutes condition for the existence of core (and equilibrium) in a two-sided matching model. Since then, this condition has often been used in the literature on matching models and equilibrium models in the presence of indivisibilities. In this paper we prove that a reservation value (or utility) function satisfies the gross substitutes condition if and only if it is an M♮-concave function defined on the unit-hypercube, which is a discrete concave function recently introduced by Murota and Shioura (1999). } } @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", keywords = "Assignment model", keywords = "Walrasian equilibrium", keywords = "Iterative auctions", keywords = "Overdemanded set", keywords = "Underdemanded set " } @book{shalev2014book, title={Understanding Machine Learning: From Theory to Algorithms}, author={Shalev-Shwartz, Shai and Ben-David, Shai}, year=2014, publisher={Cambridge University Press} } @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}, publisher={SIAM} } @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, month = jan, 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}, organization={SIAM}, 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}, publisher = {ACM}, 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}, organization={ACM}, 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}, month = {September}, 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 = {Cambridge University Press}, } @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 Berlin Heidelberg}, author={Dwork, Cynthia and Naor, Moni and Reingold, Omer and Rothblum, Guy N}, pages={735--751}, language={English} } @inproceedings{BartheO13, author = {Barthe, Gilles and Olmedo, Federico}, editor = {Fedor V. Fomin and Rusins Freivalds and Marta Z. Kwiatkowska and David Peleg}, title = {Beyond Differential Privacy: Composition Theorems and Relational Logic for $f$-divergences between Probabilistic Programs}, booktitle = icalp13, series = {Lecture Notes in Computer Science}, 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}, ADDRESS = {Berlin, Germany}, ORGANIZATION = {{IFIP}}, EDITOR = {Erika Abraham and Catuscia Palamidessi}, PUBLISHER = {{Springer}}, SERIES = {Lecture Notes in Computer Science}, 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-Verlag}, booktitle = sas14, series = {Lecture Notes in Computer Science}, volume = {8723}, url = {https://www.cs.colorado.edu/~srirams/papers/sas14-expectations.pdf} } @inproceedings{CousotM12, author = {Patrick Cousot and Michael Monerau}, editor = {Helmut Seidl}, title = {Probabilistic Abstract Interpretation}, booktitle = esop12, series = {Lecture Notes in Computer Science}, volume = {7211}, pages = {169--193}, publisher = {Springer}, year = {2012}, url = {http://www.di.ens.fr/~cousot/publications.www/Cousot-Monerau-ESOP2012-extended.pdf} }