2572 lines
76 KiB
BibTeX
2572 lines
76 KiB
BibTeX
@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},
|
||
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
|
||
}
|
||
|
||
@inproceedings{l-diversity,
|
||
author = {Machanavajjhala, A. and Gehrke, J. and Kifer, D. and Venkitasubramaniam, M.},
|
||
title = {$l$-{D}iversity: {P}rivacy beyond $k$-anonymity},
|
||
booktitle = icde06,
|
||
url = {http://dl.acm.org/citation.cfm?id=1217302},
|
||
year = 2006
|
||
}
|
||
|
||
@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{k-anon-attack,
|
||
author = {Srivatsava Ranjit Ganta and
|
||
Shiva Prasad Kasiviswanathan and
|
||
Adam Smith},
|
||
title = {Composition attacks and auxiliary information in data privacy},
|
||
booktitle = kdd08,
|
||
pages = {265--273},
|
||
year = 2008,
|
||
url = {http://arxiv.org/abs/0803.0032}
|
||
}
|
||
|
||
@inproceedings{HGH+13,
|
||
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{fuzz,
|
||
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},
|
||
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},
|
||
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}},
|
||
note = {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,
|
||
volume={46},
|
||
number={1},
|
||
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},
|
||
note = {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,
|
||
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://www.cis.upenn.edu/~justhsu/docs/dfuzztc.pdf},
|
||
jh = yes,
|
||
docs = 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,
|
||
docs = yes
|
||
}
|
||
|
||
@inproceedings{HsuTaxes,
|
||
author = {Justin Hsu},
|
||
title = {Death, Taxes, and Formal Verification (Abstract)},
|
||
year = {2015},
|
||
booktitle = snapl15,
|
||
jh = 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={MIT press Cambridge}
|
||
}
|
||
|
||
@article{Chadha:2007,
|
||
Author = {Chadha, R. and Cruz-Filipe, L. and Mateus, P. and Sernadas, A.},
|
||
Journal = tcs,
|
||
Number = {1-2},
|
||
Title = {Reasoning about probabilistic sequential programs},
|
||
Volume = {379},
|
||
Year = {2007}}
|
||
|
||
@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{Chadha:2007,
|
||
Author = {Chadha, R. and Cruz-Filipe, L. and Mateus, P. and Sernadas, A.},
|
||
Journal = tcs,
|
||
Number = {1-2},
|
||
Title = {Reasoning about probabilistic sequential programs},
|
||
Volume = {379},
|
||
Year = {2007}}
|
||
|
||
@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{DBLP:conf/itp/GonthierAABCGRMOBPRSTT13,
|
||
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'Connor 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{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},
|
||
publisher={Wiley Online Library}
|
||
}
|
||
|
||
@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
|
||
}
|
||
|
||
@unpublished{AHJ15,
|
||
title = {Online Assignment with Heterogeneous Tasks and Deadlines},
|
||
author = {Assadi, Sepehr and Hsu, Justin and Jabbari, Shahin},
|
||
year = {2015},
|
||
jh = yes
|
||
}
|
||
|
||
@unpublished{HKM-verif,
|
||
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
|
||
}
|