diff --git a/bibs/myrefs.bib b/bibs/myrefs.bib index a670de4..7c896fc 100644 --- a/bibs/myrefs.bib +++ b/bibs/myrefs.bib @@ -1,282 +1,283 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%% UNPUBLISHED %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @unpublished{HKM-verif15, - title = {Computer-aided verification in mechanism design}, + 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, + Gaboardi, Marco and + Gallego Arias, Emilio Jes{\'u}s and + Hsu, Justin and + Roth, Aaron and + Strub, Pierre-Yves}, + year = {2015}, + url = {http://arxiv.org/abs/1502.04052}, + jh = yes, eprint = yes } @unpublished{BEGGHS15, - title = {Formal certification of randomized algorithms}, + 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 + year = 2015, + jh = yes, + docs = yes } %%%%%%%%%%%%%%%%%%%%%%%%%%%% CONFERENCES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @inproceedings{HHRW16, - author = {Hsu, Justin and + author = {Hsu, Justin and Huang, Zhiyi and Roth, Aaron and Wu, Zhiwei Steven}, - title = {Jointly private convex programming}, + title = {Jointly private convex programming}, booktitle = soda16, - year = {2016}, - url = {http://arxiv.org/abs/1411.0998}, - jh = yes, - eprint = yes, - note = {To appear.} + year = {2016}, + url = {http://arxiv.org/abs/1411.0998}, + jh = yes, + eprint = yes, + note = {To appear.} } @inproceedings{BEGHSS15, - title = {Relational reasoning via probabilistic coupling}, - author = {Barthe, Gilles and + title = {Relational reasoning via probabilistic coupling}, + author = {Barthe, Gilles and Espitau, Thomas and Gr{\'e}goire, Benjamin and Hsu, Justin and Stefanesco, L{\'e}o and Strub, {P}ierre-{Y}ves}, booktitle = lpar15, - year = 2015, - jh = yes, - docs = yes, - note = {To appear.} + year = 2015, + jh = yes, + eprint = yes, + url = {http://arxiv.org/abs/1509.03476}, + note = {To appear.} } @inproceedings{AHJ15, - title = {Online assignment with heterogeneous tasks in crowdsourcing + title = {Online assignment with heterogeneous tasks in crowdsourcing markets}, - author = {Assadi, Sepehr and Hsu, Justin and Jabbari, Shahin}, - year = {2015}, + author = {Assadi, Sepehr and Hsu, Justin and Jabbari, Shahin}, + year = {2015}, booktitle = hcomp15, - url = {http://arxiv.org/abs/1508.03593}, - jh = yes, - eprint = yes, - note = {To appear.} + url = {http://arxiv.org/abs/1508.03593}, + jh = yes, + eprint = yes, + note = {To appear.} } @inproceedings{HsuTaxes, - author = {Justin Hsu}, - title = {Death, taxes, and formal verification (Abstract)}, - year = {2015}, + author = {Justin Hsu}, + title = {Death, taxes, and formal verification (Abstract)}, + year = {2015}, booktitle = snapl15, - jh = yes, - slides = yes, - docs = yes + jh = yes, + slides = yes, + docs = yes } @inproceedings{GHaccuracy, - author = {Marco Gaboardi and + author = {Marco Gaboardi and Justin Hsu}, - title = {A Theory {AB} toolbox}, - year = {2015}, + title = {A Theory {AB} toolbox}, + year = {2015}, booktitle = snapl15, - jh = yes, - slides = yes, - docs = yes + jh = yes, + slides = yes, + docs = yes } @inproceedings{BGGHRS15, - title = {Higher-order approximate relational refinement types for + title = {Higher-order approximate relational refinement types for mechanism design and differential privacy}, - author = {Barthe, Gilles and + 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 + year = {2015}, + url = {http://arxiv.org/abs/1407.6845}, + jh = yes, + slides = yes, + eprint = yes } @inproceedings{AGGH14, - author = {de Amorim, Arthur Azevedo and + 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}, + title = {Really naturally linear indexed type-checking}, booktitle = {Proceedings of Implementation of Functional Languages (IFL), Boston, Massachusetts}, - year = {2014}, - url = {http://arxiv.org/abs/1503.04522}, - jh = yes, - slides = yes, - eprint = yes + year = {2014}, + url = {http://arxiv.org/abs/1503.04522}, + jh = yes, + slides = yes, + eprint = yes } @inproceedings{BGGHKS14, - author = {Barthe, Gilles and + 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}, + title = {Proving differential privacy in {H}oare logic}, booktitle = csf14, - year = {2014}, - url = {http://arxiv.org/abs/1407.2988}, - jh = yes, - eprint = yes + year = {2014}, + url = {http://arxiv.org/abs/1407.2988}, + jh = yes, + eprint = yes } @inproceedings{HGH14, - author = {Hsu, Justin and + 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}, + 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 + year = 2014, + url = {http://arxiv.org/abs/1402.3329}, + jh = yes, + slides = yes, + eprint = yes } @inproceedings{HRRU14, - author = {Hsu, Justin and + author = {Hsu, Justin and Roth, Aaron and Roughgarden, Tim and Ullman, Jonathan}, - title = {Privately solving linear programs}, + 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}, + 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}, + 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 + jh = yes, + slides = yes, + eprint = yes } @inproceedings{GGHRW14, - author = {Gaboardi, Marco and + 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}, + 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 + year = {2014}, + url = {http://arxiv.org/abs/1402.1526}, + jh = yes, + slides = yes, + poster = yes, + eprint = yes } @inproceedings{HHRRW14, - author = {Hsu, Justin and + author = {Hsu, Justin and Huang, Zhiyi and Roth, Aaron and Roughgarden, Tim and Wu, Zhiwei Steven}, - title = {Private matchings and allocations}, + title = {Private matchings and allocations}, booktitle = stoc14, - year = {2014}, - pages = {21--30}, - url = {http://arxiv.org/abs/1311.2828}, - doi = {10.1145/2591796.2591826}, + 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}, + 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 + jh = yes, + poster = yes, + eprint = yes } @inproceedings{WHE13, - title = {Towards dependently typed {H}askell: {S}ystem {FC} with kind equality}, - author = {Weirich, Stephanie and + title = {Towards dependently typed {H}askell: {S}ystem {FC} with kind equality}, + author = {Weirich, Stephanie and Hsu, Justin and Eisenberg, Richard A}, booktitle = icfp13, - url = {http://www.cis.upenn.edu/~justhsu/docs/nokinds.pdf}, - volume = {13}, - year = {2013}, - jh = yes, - docs = yes + url = {http://www.cis.upenn.edu/~justhsu/docs/nokinds.pdf}, + volume = {13}, + year = {2013}, + jh = yes, + docs = yes } @inproceedings{HRU13, - title = {Differential privacy for the analyst via private equilibrium computation}, - author = {Hsu, Justin and + 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}, + url = {http://arxiv.org/abs/1211.0877}, booktitle = stoc13, - pages = {341--350}, - year = {2013}, - jh = yes, - slides = yes, - eprint = yes + pages = {341--350}, + year = {2013}, + jh = yes, + slides = yes, + eprint = yes } @inproceedings{GGHHP13, - title = {Automatic sensitivity analysis using linear dependent types}, - author = {Gaboardi, Marco and + 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}, + url = {http://fopara2013.cs.unibo.it/paper_8.pdf}, booktitle = fopara, - year = {2013}, - jh = yes + year = {2013}, + jh = yes } @inproceedings{GHHNP13, - title = {Linear dependent types for differential privacy}, - author = {Gaboardi, Marco and + 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 + pages = {357--370}, + url = {http://dl.acm.org/citation.cfm?id=2429113}, + year = {2013}, + jh = yes, + docs = yes } @inproceedings{HKR12, - title = {Distributed private heavy hitters}, - author = {Hsu, Justin and + title = {Distributed private heavy hitters}, + author = {Hsu, Justin and Khanna, Sanjeev and Roth, Aaron}, booktitle = icalp12, - pages = {461--472}, - year = {2012}, + 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 + 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 + jh = yes, + slides = yes, + eprint = yes } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% JOURNALS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -340,12 +341,12 @@ } @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} + 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, @@ -551,298 +552,299 @@ } @inproceedings{airavat, - author = {Indrajit Roy and Srinath Setty and Ann Kilzer and Vitaly + 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 + 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 + 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 + 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 + 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 + 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} + 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} + 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 + 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} + title = {Robust De-anonymization of Large Sparse Datasets}, + booktitle = sp08, + year = {2008}, + pages = {111--125}, + url = {http://arxiv.org/abs/cs/0610105} } @inproceedings{BLST10, - author = {Raghav Bhaskar and - Srivatsan Laxman and - Adam Smith and - Abhradeep Thakurta}, - title = {Discovering frequent patterns in sensitive data}, - booktitle = kdd10, - pages = {503--512}, - year = 2010, - url = {http://dl.acm.org/citation.cfm?id=1835869} + 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} + 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} + 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{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} +@article{certipriv, + author = {Gilles Barthe and + Boris K{\"{o}}pf and + Federico Olmedo and + Santiago Zanella B{\'{e}}guelin}, + title = {Probabilistic Relational Reasoning for Differential Privacy}, + journal = toplas, + volume = {35}, + number = {3}, + pages = {9}, + year = {2013}, + url = {http://software.imdea.org/~bkoepf/papers/toplas13.pdf}, } @inproceedings{ReedPierce10, - author = {Jason Reed and Benjamin C Pierce}, - title = {Distance Makes the Types Grow Stronger: {A} Calculus for + 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} + 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} + 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 + 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} + 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} + 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 + 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} + 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 + 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} + 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} + 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} + 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} + 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 + title = {Privacy, accuracy, and consistency too: a holistic solution to contingency table release}, - author = {Barak, Boaz and Chaudhuri, Kamalika and Dwork, Cynthia and Kale, + 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} + 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} + 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} + 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 + 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 + 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} + 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} + 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} + 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} + 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 + 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} + 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, @@ -856,31 +858,31 @@ } @inproceedings{RR10, - author = {Aaron Roth and + 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}, + 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} + 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, + 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} + 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, @@ -894,71 +896,71 @@ } @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} + 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 + 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} + 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} + 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 + 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} + 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} + 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 + author = {Grigory Yaroslavtsev and Graham Cormode and Cecilia M. Procopiuc and Divesh Srivastava}, - title = {Accurate and efficient private release of datacubes and + 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} + booktitle = icde13, + year = {2013}, + pages = {745--756}, + url = {http://doi.ieeecomputersociety.org/10.1109/ICDE.2013.6544871} } @inproceedings{CV13, @@ -977,8 +979,7 @@ 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}, + url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.90.7354&rep=rep1&type=pdf}, year = {2001} } @@ -993,44 +994,44 @@ } @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} + 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 + 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} + 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} + 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, + 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} + 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, @@ -1040,111 +1041,110 @@ booktitle = popl04, pages = {281--292}, year = 2004, - url = - {http://www.cs.cmu.edu/~joshuad/papers/tridirectional-typechecking/Dunfield04_tridirectional.pdf} + 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} + 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 +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} +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} + 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} + 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} + 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} + 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} + 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} + 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} + 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} + 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}, + Author = {Ramsey, Norman and Pfeffer, Avi}, Booktitle = popl02, - Pages = {154--165}, + 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} + Title = {Stochastic lambda calculus and monads of probability distributions}, + Year = {2002}, + url = {http://www.cs.tufts.edu/~nr/pubs/pmonad.pdf} } @@ -1160,22 +1160,22 @@ url={http://goto.ucsd.edu/~nvazou/refinement_types_for_haskell.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} + 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.}, + 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}} + Series = {Monographs in Computer Science}, + Title = {Abstraction, Refinement, and Proof for Probabilistic Systems}, + Year = {2005}} @inproceedings{Borgstrom:2011, author = {Johannes Borgstr{\"o}m and @@ -1209,1004 +1209,986 @@ url={http://goto.ucsd.edu/~nvazou/refinement_types_for_haskell.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} + 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} +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}, + author = {Giry, Mich\`{e}le}, journal = {Categorical Aspects of Topology and Analysis}, - pages = {68--85}, - title = {{A categorical approach to probability theory}}, - year = {1982}, + 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} + 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} + 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} + 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} + 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} + title = {Probabilistic relational verification for cryptographic implementations}, + author = {Barthe, Gilles and Fournet, C{\'e}dric and Gr{\'e}goire, Benjamin and Strub, {P}ierre-{Y}ves and Swamy, Nikhil and Zanella-B{\'e}guelin, Santiago}, + booktitle = popl14, + pages = {193--206}, + year = {2014}, + url = {http://research.microsoft.com/en-us/um/people/nswamy/papers/rfstar.pdf} } @INPROCEEDINGS{polymonad, - TITLE = {Polymonadic Programming}, - AUTHOR = {Michael Hicks and Gavin Bierman and Nataliya Guts and Daan Leijen and Nikhil Swamy}, + 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} + 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} + 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} + 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 + 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} + 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} + 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 + author = {Gilles Barthe and Benjamin Gr{\'e}goire and Sylvain Heraud and Santiago Zanella B{\'e}guelin}, - title = {Computer-Aided Security Proofs for the Working Cryptographer}, - booktitle = crypto11, - year = {2011}, - pages = {71--90}, - url = {http://software.imdea.org/~szanella/Zanella.2011.CRYPTO.pdf}, - bibsource = {DBLP, http://dblp.uni-trier.de} + title = {Computer-Aided Security Proofs for the Working Cryptographer}, + booktitle = crypto11, + year = {2011}, + pages = {71--90}, + url = {http://software.imdea.org/~szanella/Zanella.2011.CRYPTO.pdf}, + bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{BartheDGKZ13, - author = {Gilles Barthe and + 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 + 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} + 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 + 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}, + 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 + author = {Wei Bai and Emmanuel M Tadjouddine and Terry R Payne and Sheng-Uei Guan}, - title = {A Proof-Carrying Code Approach to Certificate Auction Mechanisms}, - booktitle = {FACS}, - year = {2013}, - pages = {23--40}, - url = {http://dx.doi.org/10.1007/978--3-319--07602--7_4}, - publisher = springer, - series = lncs, - volume = {8348}, + title = {A Proof-Carrying Code Approach to Certificate Auction Mechanisms}, + booktitle = {FACS}, + year = {2013}, + pages = {23--40}, + url = {http://dx.doi.org/10.1007/978--3-319--07602--7_4}, + publisher = springer, + series = lncs, + volume = {8348}, } @inproceedings{DBLP:conf/ceemas/TadjouddineG07, - author = {Emmanuel M Tadjouddine and + author = {Emmanuel M Tadjouddine and Frank Guerin}, - title = {Verifying Dominant Strategy Equilibria in Auctions}, - booktitle = ceemas07, - year = {2007}, - pages = {288--297}, - url = {http://dx.doi.org/10.1007/978--3-540--75254--7_29}, - publisher = springer, - series = lncs, - volume = {4696}, + title = {Verifying Dominant Strategy Equilibria in Auctions}, + booktitle = ceemas07, + year = {2007}, + pages = {288--297}, + url = {http://dx.doi.org/10.1007/978--3-540--75254--7_29}, + publisher = springer, + series = lncs, + volume = {4696}, } @article{DBLP:journals/ipl/Vestergaard06, - author = {Ren{\'e} Vestergaard}, - title = {A constructive approach to sequential Nash equilibria}, - journal = {Inf. Process. Lett.}, - volume = {97}, - number = {2}, - year = {2006}, - pages = {46--51}, - url = {http://dx.doi.org/10.1016/j.ipl.2005.09.010}, - bibsource = {DBLP, http://dblp.uni-trier.de} + 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} + 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} +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} +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} + 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 + author = {Christoph Lange and + Marco B Caminati and + Manfred Kerber and + Till Mossakowski and + Colin Rowat and + Makarius Wenzel and + Wolfgang Windsteiger}, + title = {A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory}, - booktitle = {MKM/Calculemus/DML}, - publisher = springer, - series = lncs, - volume = {7961}, - year = {2013}, - pages = {200--215}, - url = {http://dx.doi.org/10.1007/978--3-642--39320--4_13} + booktitle = {MKM/Calculemus/DML}, + publisher = springer, + series = lncs, + volume = {7961}, + year = {2013}, + pages = {200--215}, + url = {http://dx.doi.org/10.1007/978--3-642--39320--4_13} } @article{DBLP:journals/cacm/ChaudhuriGL12, - author = {Swarat Chaudhuri and - Sumit Gulwani and - Roberto Lublinerman}, - title = {Continuity and robustness of programs}, - journal = cacm, - volume = {55}, - number = {8}, - year = {2012}, - pages = {107--115}, - url = {http://dl.acm.org/citation.cfm?id=2240262} + author = {Swarat Chaudhuri and + Sumit Gulwani and + Roberto Lublinerman}, + title = {Continuity and robustness of programs}, + journal = cacm, + volume = {55}, + number = {8}, + year = {2012}, + pages = {107--115}, + url = {http://dl.acm.org/citation.cfm?id=2240262} } @article{BartheDR04, - title={Secure information flow by self-composition}, - author={Barthe, Gilles and - D'Argenio, Pedro R and - Rezk, Tamara}, - journal=mscs, - volume={21}, - number={06}, - pages={1207--1252}, - year={2011}, - publisher=cup, - url = {http://www-sop.inria.fr/lemme/Tamara.Rezk/publication/Barthe-DArgenio-Rezk-Journal.pdf} + title = {Secure information flow by self-composition}, + author = {Barthe, Gilles and + D'Argenio, Pedro R and + Rezk, Tamara}, + journal = mscs, + volume = {21}, + number = {06}, + pages = {1207--1252}, + year = {2011}, + publisher = cup, + url = {http://www-sop.inria.fr/lemme/Tamara.Rezk/publication/Barthe-DArgenio-Rezk-Journal.pdf} } @inproceedings{ZaksP08, - author = {Anna Zaks and Amir Pnueli}, - title = {{CoVaC}: Compiler Validation by Program Analysis of the Cross-Product}, - booktitle = fm08, - pages = {35--51}, - publisher = springer, - address = {Heidelberg}, - series = lncs, - volume = {5014}, - year = {2008}, - url = {http://llvm.org/pubs/2008-05-CoVaC.pdf} + author = {Anna Zaks and Amir Pnueli}, + title = {{CoVaC}: Compiler Validation by Program Analysis of the Cross-Product}, + booktitle = fm08, + pages = {35--51}, + publisher = springer, + address = {Heidelberg}, + series = lncs, + volume = {5014}, + year = {2008}, + url = {http://llvm.org/pubs/2008-05-CoVaC.pdf} } @inproceedings{TerauchiA05, - Address = {Heidelberg}, - Author = {Terauchi, Tachio and Aiken, Alex}, - Booktitle = sas05, - Pages = {352--367}, - Publisher = springer, - Series = lncs, - Title = {Secure Information Flow as a Safety Problem}, - Volume = {3672}, - Year = {2005}, - url = {http://theory.stanford.edu/~aiken/publications/papers/sas05b.pdf} + Address = {Heidelberg}, + Author = {Terauchi, Tachio and Aiken, Alex}, + Booktitle = sas05, + Pages = {352--367}, + Publisher = springer, + Series = lncs, + Title = {Secure Information Flow as a Safety Problem}, + Volume = {3672}, + Year = {2005}, + url = {http://theory.stanford.edu/~aiken/publications/papers/sas05b.pdf} } @inproceedings{BartheCK11, - author = {Gilles Barthe and + author = {Gilles Barthe and Juan Manuel Crespo and C{\'e}sar Kunz}, - title = {Relational Verification Using Product Programs}, - booktitle = fm11, - year = {2011}, - pages = {200--214}, - url = {http://software.imdea.org/~ckunz/rellog/long-rellog.pdf}, + title = {Relational Verification Using Product Programs}, + booktitle = fm11, + year = {2011}, + pages = {200--214}, + url = {http://software.imdea.org/~ckunz/rellog/long-rellog.pdf}, } @inproceedings{BartheCK13, - author = {Gilles Barthe and - Juan Manuel Crespo and - C{\'e}sar Kunz}, - title = {Beyond 2-Safety: Asymmetric Product Programs for Relational + author = {Gilles Barthe and + Juan Manuel Crespo and + C{\'e}sar Kunz}, + title = {Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification}, - booktitle = lfcompsci13, - year = {2013}, - pages = {29--43}, - url = {http://dx.doi.org/10.1007/978--3-642--35722--0_3}, - bibsource = {DBLP, http://dblp.uni-trier.de} + booktitle = lfcompsci13, + year = {2013}, + pages = {29--43}, + url = {http://dx.doi.org/10.1007/978--3-642--35722--0_3}, + bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DBLP:conf/esop/KnowlesF07, - author = {Kenneth Knowles and - Cormac Flanagan}, - title = {Type Reconstruction for General Refinement Types}, - booktitle = esop07, - year = {2007}, - pages = {505--519}, - url = {http://users.soe.ucsc.edu/~cormac/papers/esop07.pdf} + 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} + 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} + 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} + 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} + 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 + 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 = + 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} + 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: + 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} + 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} + 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} + 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}, + 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} + year = {2006}, + pages = {93--104}, + url = {http://galois.com/wp-content/uploads/2014/07/pub_AT_SAGEHybridChecking.pdf} } @inproceedings{EignerM13, - author = {Fabienne Eigner and + 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} + 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 + 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} + 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 + 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} + 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 + 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} + 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 + 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} + 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 + 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", + 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 + 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} + 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} + 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} + 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 + 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} + 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} + 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} + 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} + 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} + 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 + 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} + 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 + 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 + 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} + 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} + 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} + title = {Truthful mechanisms for agents that value privacy}, + author = {Chen, Yiling and Chong, Stephen and Kash, Ian A and Moran, Tal and Vadhan, Salil}, + booktitle = ec13, + pages = {215--232}, + year = {2013}, + url = {http://arxiv.org/abs/1111.5472} } @inproceedings{Xia13, - title={Is privacy compatible with truthfulness?}, - author={Xiao, David}, - booktitle=itcs13, - pages={67--86}, - year={2013}, - url={https://eprint.iacr.org/2011/005} + title = {Is privacy compatible with truthfulness?}, + author = {Xiao, David}, + booktitle = itcs13, + pages = {67--86}, + year = {2013}, + url = {https://eprint.iacr.org/2011/005} } @inproceedings{IOh01, - title={{BI} as an assertion language for mutable data structures}, - author={Ishtiaq, Samin S and O'Hearn, Peter W}, - booktitle=popl01, - year=2001, - url={http://dl.acm.org/citation.cfm?id=375719}, - pages={14--26} + 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} + 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} + 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 + 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} + 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} + 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} + 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} + 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} + 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 + 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} + 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 + 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} + 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} + 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} + 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} + 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} + 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} + 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} + 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 + 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} + booktitle = itcs10, + pages = {66--80}, + url = {http://www.cs.toronto.edu/~toni/Papers/panprivacy.pdf}, + year = {2010} } @inproceedings{recommender, - title = {Differentially private recommender systems: building privacy into the net}, - author = {McSherry, Frank and Mironov, Ilya}, - booktitle = kdd09, - pages = {627--636}, - year = {2009}, - url = {http://research.microsoft.com/pubs/80511/netflixprivacy.pdf} + 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}, + 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 + title = {Concentration of measure for the analysis of randomized algorithms}, + author = {Dubhashi, Devdatt P and Panconesi, Alessandro}, + year = {2009}, + publisher = cup } @article{LovaszLocal, - title={Problems and results on 3-chromatic hypergraphs and some related + 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} + 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} + 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 + 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}, + 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 + author = {Michael Carbin and Deokhwan Kim and Sasa Misailovic and Martin C Rinard}, - title = {Proving acceptability properties of relaxed nondeterministic approximate + 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}, + 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 + 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 + 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}, + 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 + author = {Michael Carbin and Deokhwan Kim and Sasa Misailovic and Martin C Rinard}, - title = {Proving acceptability properties of relaxed nondeterministic approximate + 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}, + booktitle = pldi12, + pages = {169--180}, + year = {2012}, + url = {http://doi.acm.org/10.1145/2254064.2254086}, } @InProceedings{Necula97, - author = "G. C. Necula", - title = "Proof-carrying code", - booktitle = popl97, - year = "1997", - pages = "106--119", - publisher = {ACM} + author = "G. C. Necula", + title = "Proof-carrying code", + booktitle = popl97, + year = "1997", + pages = "106--119", + publisher = {ACM} } @inproceedings{BartheGHZ11, - author = {Gilles Barthe and + author = {Gilles Barthe and Benjamin Gr{\'e}goire and Sylvain Heraud and Santiago Zanella B{\'e}guelin}, - title = {Computer-Aided Security Proofs for the Working Cryptographer}, - Booktitle = crypto11, - year = {2011}, - Pages = {71--90}, - publisher = springer, - series = lncs, - volume = {6841} + title = {Computer-Aided Security Proofs for the Working Cryptographer}, + Booktitle = crypto11, + year = {2011}, + Pages = {71--90}, + publisher = springer, + series = lncs, + volume = {6841} } @inproceedings{flanagan2001, - title={Avoiding exponential explosion: Generating compact + title = {Avoiding exponential explosion: Generating compact verification conditions}, - author={Flanagan, Cormac and Saxe, James B}, - booktitle=popl01, - pages={193--205}, - year={2001}, - publisher={ACM} + author = {Flanagan, Cormac and Saxe, James B}, + booktitle = popl01, + pages = {193--205}, + year = {2001}, + publisher = {ACM} } @inproceedings{BartheDGKSS13, @@ -2230,267 +2212,267 @@ verification conditions}, } @article{Hoare69, - author = {C. A. R. Hoare}, - title = {An Axiomatic Basis for Computer Programming}, - journal = cacm, - year = {1969}, - volume = {12}, - number = {10} + 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} + 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} + 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} + 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 + 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} + 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} + 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.} + 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 + 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} + 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} + 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} + 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} + 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 + title = {Selfish routing and the price of anarchy}, + author = {Roughgarden, Tim}, + volume = {174}, + year = {2005}, + publisher = mitpress } @article{Morgan:1996, - author = {C Morgan and + author = {C Morgan and A Mc{I}ver and K Seidel}, - title = {Probabilistic Predicate Transformers}, - journal = toplas, - volume = {18}, - number = {3}, - year = {1996} + 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} + author = {D. Kozen}, + title = {A Probabilistic {PDL}}, + journal = jcss, + volume = {30}, + number = {2}, + year = {1985} } @article{Morgan:1996, - author = {C Morgan and + author = {C Morgan and A Mc{I}ver and K Seidel}, - title = {Probabilistic Predicate Transformers}, - journal = toplas, - volume = {18}, - number = {3}, - year = {1996} + 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} + 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} +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 + 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}, + 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 + 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}, + 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 + 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 + title = {A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory}, - booktitle={Intelligent Computer Mathematics}, - publisher = springer, - series = lncs, - volume = {7961}, - year = {2013}, - pages = {200--215}, - url = {http://dx.doi.org/10.1007/978--3-642--39320--4_13}, - publisher=springer + booktitle = {Intelligent Computer Mathematics}, + publisher = springer, + series = lncs, + volume = {7961}, + year = {2013}, + pages = {200--215}, + url = {http://dx.doi.org/10.1007/978--3-642--39320--4_13}, + publisher = springer } @article{DBLP:journals/ipl/Vestergaard06, - author = {Ren{\'e} Vestergaard}, - title = {A constructive approach to sequential Nash equilibria}, - journal = {Inf. Process. Lett.}, - volume = {97}, - number = {2}, - year = {2006}, - pages = {46--51}, - url = {http://dx.doi.org/10.1016/j.ipl.2005.09.010}, - bibsource = {DBLP, http://dblp.uni-trier.de} + 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 + 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}, + 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 + 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", + 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 + author = {Georges Gonthier and Andrea Asperti and Jeremy Avigad and Yves Bertot and @@ -2505,44 +2487,44 @@ language={English} 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}, + 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 + 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} + title = {Incentives in teams}, + author = {Groves, Theodore}, + journal = {Econometrica: Journal of the Econometric Society}, + pages = {617--631}, + year = {1973} } @inproceedings{Bellare:2006, - address = {Heidelberg}, - author = {Bellare, Mihir and Rogaway, Phillip}, - booktitle = eucrypt06, - pages = {409--426}, - publisher = springer, - series = lncs, - title = {The Security of Triple Encryption and a Framework for + address = {Heidelberg}, + author = {Bellare, Mihir and Rogaway, Phillip}, + booktitle = eucrypt06, + pages = {409--426}, + publisher = springer, + series = lncs, + title = {The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs}, - volume = {4004}, - year = {2006}, - url = {https://www.iacr.org/archive/eurocrypt2006/40040415/40040415.pdf} + volume = {4004}, + year = {2006}, + url = {https://www.iacr.org/archive/eurocrypt2006/40040415/40040415.pdf} } @misc{Halevi:2005, @@ -2562,479 +2544,479 @@ language={English} } @unpublished{Naumann:2009, - author = {Naumann, David A}, - title = {Theory for software verification}, - year = {2009}, - url = {http://www.cs.stevens.edu/~naumann/publications/theoryverif.pdf} + 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 + 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}, + booktitle = {Handbook of satisfiability}, + volume = {185}, + year = {2009}, + publisher = {IOS press}, } @inproceedings{HPN11, - title={Differential Privacy Under Fire}, - author={Haeberlen, Andreas and + title = {Differential Privacy Under Fire}, + author = {Haeberlen, Andreas and Pierce, Benjamin C and Narayan, Arjun}, - booktitle={USENIX Security Symposium}, - year={2011} + 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} + 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}, + 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} + 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 + 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, + 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", + 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", + 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, + 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 + 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}, + 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", + 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 + author = "Keven Watkins and Iliano Cervesato and Frank Pfenning and David Walker", - title = "A concurrent logical framework {I}: The propositional + title = "A concurrent logical framework {I}: The propositional fragment", - booktitle = types, - volume = 3085, - series = lncs, - publisher = springer, - year = "2003", + booktitle = types, + volume = 3085, + series = lncs, + publisher = springer, + year = "2003", } @InProceedings{DLG11, -author= {Dal Lago, Ugo and +author = {Dal Lago, Ugo and Gaboardi, Marco}, -title="Linear Dependent Types and Relative Completeness", - booktitle = lics11, - pages = "133--142", -year={2011} +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, + 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 + 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} + 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}, + 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 + 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 + 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", + 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} + 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}, + 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}, + 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} + 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}, + 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 + 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} + 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, + 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 + 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 + 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}, + booktitle = kdd08, + pages = {265--273}, + year = {2008}, } @book{Hurwicz60, - title={Optimality and informational efficiency in resource allocation + title = {Optimality and informational efficiency in resource allocation processes}, - author={Hurwicz, Leonid}, - year={1960}, - publisher={Stanford University Press} + 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}, + 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} + 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} + 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, + 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 + 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} + 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} + 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 + 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 + 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 + 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} + 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}, + 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 + 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 + 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 + 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} + 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 + 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 + 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}, + title = {Liquid types}, + author = {Rondon, Patrick M and Kawaguci, Ming and Jhala, Ranjit}, + booktitle = pldi08, + volume = {43}, + number = {6}, + pages = {159--169}, + year = {2008}, } @book{Thorisson00, - author = {Hermann Thorisson}, - title = {Coupling, Stationarity, and Regeneration}, - publisher = springer, - year = {2000} + author = {Hermann Thorisson}, + title = {Coupling, Stationarity, and Regeneration}, + publisher = springer, + year = {2000} } @book{Lindvall02, - title={Lectures on the coupling method}, - author={Lindvall, Torgny}, - year={2002}, - publisher={Courier Corporation} + title = {Lectures on the coupling method}, + author = {Lindvall, Torgny}, + year = {2002}, + publisher = {Courier Corporation} } @book{Villani08, - title={Optimal transport: old and new}, - author={Villani, C{\'e}dric}, - year={2008}, - publisher={Springer Science} + title = {Optimal transport: old and new}, + author = {Villani, C{\'e}dric}, + year = {2008}, + publisher = {Springer Science} } @techreport{DengD11, - Author = {Deng, Yuxin and Du, Wenjie}, - Institution = {Carnegie Mellon University}, - Month = {March}, - Number = {CMU-CS-11-110}, - Title = {Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation}, - Year = {2011}, - url = {http://arxiv.org/abs/1103.4577} + Author = {Deng, Yuxin and Du, Wenjie}, + Institution = {Carnegie Mellon University}, + Month = {March}, + Number = {CMU-CS-11-110}, + Title = {Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation}, + Year = {2011}, + url = {http://arxiv.org/abs/1103.4577} } @article{Yang07, - author = {H. Yang}, - title = {Relational separation logic}, - journal = tcs, - volume = 375, - number = {1-3}, - year = 2007, - pages = {308--334}, - url = {http://www.cs.ox.ac.uk/people/hongseok.yang/paper/data.pdf} + author = {H. Yang}, + title = {Relational separation logic}, + journal = tcs, + volume = 375, + number = {1-3}, + year = 2007, + pages = {308--334}, + url = {http://www.cs.ox.ac.uk/people/hongseok.yang/paper/data.pdf} } @article{mufa1994optimal, - title={Optimal Markovian couplings and applications}, - author={Mufa, Chen}, - journal={Acta Mathematica Sinica}, - volume={10}, - number={3}, - pages={260--275}, - year={1994}, - publisher=springer + title = {Optimal Markovian couplings and applications}, + author = {Mufa, Chen}, + journal = {Acta Mathematica Sinica}, + volume = {10}, + number = {3}, + pages = {260--275}, + year = {1994}, + publisher = springer } diff --git a/content/news.md b/content/news.md index e011c87..966511f 100644 --- a/content/news.md +++ b/content/news.md @@ -1,3 +1,5 @@ ++ **09/2015** Our preprint **Relational reasoning via probabilistic coupling** +is now available on `arXiv`. + **09/2015** Our paper **Jointly private convex programming** has been accepted to **SODA 2016**! + **09/2015** Our paper **Relational reasoning via probabilistic coupling** diff --git a/files/docs/BEGHSS15paper.pdf b/files/docs/BEGHSS15paper.pdf deleted file mode 100644 index 278314d..0000000 Binary files a/files/docs/BEGHSS15paper.pdf and /dev/null differ