%%%%%%%%%%%%%%%%%%%%%%%%%%%% UNPUBLISHED %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @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{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, note = {To appear.} } @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, eprint = yes, url = {http://arxiv.org/abs/1509.03476}, note = {To appear.} } @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, note = {To appear.} } @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 = {Proceedings of Implementation of Functional 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}, doi = {10.1007/978-3-662-43948-7_51}, 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}, doi = {10.1145/2591796.2591826}, 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}, doi = {10.2307/1913392}, number = {6}, urldate = {2013--07--07}, journal = {{Econometrica}}, author = {Kelso, Alexander and Crawford, Vincent}, year = {1982}, pages = {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}, doi = {10.1109/FOCS.2012.87}, 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}, doi = {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 = {Gilles Barthe and Boris K{\"{o}}pf and Federico Olmedo and Santiago Zanella B{\'{e}}guelin}, 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, doi = {10.1287/moor.20.2.257} } @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{BartheGHZ11, author = {Gilles Barthe and Benjamin Gr{\'e}goire and Sylvain Heraud and Santiago Zanella B{\'e}guelin}, title = {Computer-Aided Security Proofs for the Working Cryptographer}, booktitle = crypto11, year = {2011}, pages = {71--90}, url = {http://software.imdea.org/~szanella/Zanella.2011.CRYPTO.pdf}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{BartheDGKZ13, author = {Gilles Barthe and George Danezis and Benjamin Gr{\'e}goire and C{\'e}sar Kunz and Santiago Zanella B{\'e}guelin}, 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)}, journal = entcs, volume = "276", number = "0", pages = {61--79}, year = "2011", issn = "1571--0661", doi = "http://dx.doi.org/10.1016/j.entcs.2011.09.015", url = "http://www.sciencedirect.com/science/article/pii/S157106611100106X", author = "Michael Carl Tschantz and Dilsun Kaynar and Anupam Datta", } @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}, doi = {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 Coq}, 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}, doi = {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 = {Gilles Barthe and Benjamin Gr{\'e}goire and Sylvain Heraud and Santiago Zanella B{\'e}guelin}, title = {Computer-Aided Security Proofs for the Working Cryptographer}, Booktitle = crypto11, year = {2011}, Pages = {71--90}, publisher = springer, series = lncs, volume = {6841} } @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}, doi = {10.1007/978-3-540-93920-7_13}, 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}, doi = {10.1007/978-3-642-39634-2_14}, } @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}, doi = {http://doi.acm.org/10.1145/1707801.1706308}, } @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}, doi = {http://doi.acm.org/10.1145/1375581.1375606}, 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, doi = {10.1007/978-3-642-22012-8_4}, 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}, organization = springer } @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}, 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 }