@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{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{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{WHE13, title = {Towards dependently typed {H}askell: System {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{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{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{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 } @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.pdf} } @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} } @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{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}, booktitle = popl12, year = {2012}, pages = {97--110}, numpages = {14}, keywords = {coq proof assistant, differential privacy, relational hoare logic}, url = {http://dl.acm.org/citation.cfm?id=2103670} } @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 = nips2013, 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{BGZ09, Address = {New York}, Author = {Barthe, Gilles and Gr{\'e}goire, Benjamin and {Zanella-B{\'e}guelin}, Santiago}, Booktitle = popl09, Title = {Formal Certification of Code-Based Cryptographic Proofs}, Year = {2009}, url = {http://research.microsoft.com/pubs/185309/Zanella.2009.POPL.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://dx.doi.org/10.1007/978--3-642--22792--9_5}, 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 = {Lecture Notes in Computer Science}, 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 = {Lecture Notes in Computer Science}, 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 = {Lecture Notes in Computer Science}, 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} } @inproceedings{BartheDR04, author = {Gilles Barthe and Pedro R. D'Argenio and Tamara Rezk}, title = {Secure Information Flow by Self-Composition}, booktitle = csf04, year = {2004}, pages = {100--114}, url = {http://doi.ieeecomputersociety.org/10.1109/CSFW.2004.17}, bibsource = {DBLP, http://dblp.uni-trier.de} } @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 = {Lecture Notes in Computer Science}, 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 = {Lecture Notes in Computer Science}, 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://dx.doi.org/10.1007/978--3-642--21437--0_17}, bibsource = {DBLP, http://dblp.uni-trier.de} } @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 = lfcs13, 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{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{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{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{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{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{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{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{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{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 } @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, eprint = yes, } @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{GHaccuracy, author = {Marco Gaboardi and Justin Hsu}, title = {A Theory {AB} Toolbox}, year = {2015}, booktitle = snapl15, jh = yes, slides = yes, docs = yes } @inproceedings{HsuTaxes, author = {Justin Hsu}, title = {Death, Taxes, and Formal Verification (Abstract)}, year = {2015}, booktitle = snapl15, jh = yes, slides = yes, docs = yes } @InProceedings{Necula97, author = "G. C. Necula", title = "Proof-carrying code", booktitle = popl97, year = "1997", pages = "106--119", publisher = {ACM} } @inproceedings{Barthe11, Author = {Gilles Barthe and Benjamin Gr{\'e}goire and Sylvain Heraud and Santiago Zanella B{\'e}guelin}, Booktitle = crypto11, Pages = {71-90}, Title = {Computer-Aided Security Proofs for the Working Cryptographer}, Year = {2011}} @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}, title = {Easy{C}rypt: {A} Tutorial}, booktitle = {Foundations of Security Analysis and Design {VII} - {FOSAD} 2012/2013 Tutorial Lectures}, pages = {146--166}, series = {LNCS}, year = {2014}, volume = {8604}, publisher = {Springer} } @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 = {Lecture Notes in Computer Science}, 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 = {Lecture Notes in Computer Science}, 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}, } @unpublished{HHRW15, author = {Hsu, Justin and Huang, Zhiyi and Roth, Aaron and Wu, Zhiwei Steven}, title = {Jointly private convex programming}, year = {2015}, url = {http://arxiv.org/abs/1411.0998}, jh = yes, eprint = yes } @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 } @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 } @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}, } @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, } @unpublished{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}, year = 2015, jh = yes, docs = yes, }