justin-site/bibs/myrefs.bib

%%%%%%%%%%%%%%%%%%%%%%%%%%%% UNPUBLISHED %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@unpublished{AH17,
  title = {Synthesizing Coupling Proofs of Differential Privacy},
  author = {Albarghouthi, Aws and
            Hsu, Justin},
  year = 2017,
  note = {In submission.}
}

@unpublished{BEGHS16,
  title  = {Proving expected sensitivity of probabilistic programs},
  author = {Barthe, Gilles and
            Espitau, Thomas and
            Gr{\'e}goire, Benjamin and
            Hsu, Justin and
            Strub, {P}ierre-{Y}ves},
  year   = 2017,
  jh     = yes,
  url    = {http://arxiv.org/abs/1708.02537},
  note   = {In submission.}
}

@unpublished{BEGGHS16,
  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   = 2016,
  jh     = yes,
  url    = {http://justinh.su/files/papers/ellora.pdf},
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% JOURNALS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@article{GGHRW14,
  author    = {Gaboardi, Marco and
               Gallego Arias, Emilio Jes{\'u}s and
               Hsu, Justin and
               Roth, Aaron and
               Wu, Zhiwei Steven},
  title     = {Dual Query: Practical private query release for high dimensional data},
	journal   = jpc,
  year      = {2017},
  month     = {},
  volume    = {7},
  number    = {2},
  pages     = {53--77},
  url       = {http://arxiv.org/abs/1402.1526},
  publisher = bepress,
  jh        = yes,
  reviewed  = yes,
  poster    = {http://justinh.su/files/posters/dualquery.pdf},
  note      = "Previously published in " # icml14 # ", 2014."
}

@article{HHRRW14,
  author    = {Hsu, Justin and
               Huang, Zhiyi and
               Roth, Aaron and
               Roughgarden, Tim and
               Wu, Zhiwei Steven},
  title     = {Private matchings and allocations},
	journal   = siamjc,
  year      = {2016},
  month     = {},
  volume    = {45},
  number    = {6},
  pages     = {1953--1984},
  doi       = {10.1137/15100271X},
  url       = {http://arxiv.org/abs/1311.2828},
  jh        = yes,
  reviewed  = yes,
  poster    = {http://justinh.su/files/posters/matchings.pdf},
  note      = "Previously published in " # stoc14 # ", 2014."
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%% CONFERENCES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@inproceedings{BEHSS17,
  title  = {$\star$-Liftings for differential privacy},
  author = {Barthe, Gilles and
            Espitau, Thomas and
            Hsu, Justin and
            Sato, Tetsuya and
            Strub, {P}ierre-{Y}ves},
  booktitle = icalp17,
  year   = 2017,
  pages ={102:1--102:12},
  series = lipics,
  volume = 80,
  publisher = dagstuhl,
  url    = {https://arxiv.org/abs/1705.00133},
  slides = {http://justinh.su/files/slides/star-lifting.pdf},
  jh     = yes,
  plclub    = yes,
  reviewed = yes,
}

@inproceedings{BEGHS17,
  title  = {Proving uniformity and independence by self-composition and coupling},
  author = {Barthe, Gilles and
            Espitau, Thomas and
            Gr{\'e}goire, Benjamin and
            Hsu, Justin and
            Strub, {P}ierre-{Y}ves},
  booktitle = lpar17,
  pages  = {385--403},
  series = epic,
  volume = 46,
  year   = 2017,
  url    = {https://arxiv.org/abs/1701.06477},
  slides = {http://justinh.su/files/slides/unifindep-couple.pdf},
  jh     = yes,
  plclub    = yes,
  reviewed = yes,
}

@inproceedings{BGHS16,
  title  = {Coupling proofs are probabilistic product programs},
  author = {Barthe, Gilles and
            Gr{\'e}goire, Benjamin and
            Hsu, Justin and
            Strub, {P}ierre-{Y}ves},
  booktitle = popl17,
  year   = 2017,
  url    = {http://arxiv.org/abs/1607.03455},
  slides = {http://justinh.su/files/slides/products.pdf},
  jh     = yes,
  plclub    = yes,
  reviewed = yes,
  acceptance = {64/282=0.22},
}

@inproceedings{ACGHK16,
  title  = {A semantic account of metric preservation},
  author = {de Amorim, Arthur Azevedo and
            Gaboardi, Marco and
            Hsu, Justin and
            Katsumata, {Shin-ya} and
            Cherigui, Ikram},
  booktitle = popl17,
  year   = 2017,
  pages     = {545--556},
  url    = {http://arxiv.org/abs/1702.00374},
  jh     = yes,
  plclub    = yes,
  reviewed = yes,
  acceptance = {64/282=0.22},
}

@inproceedings{HKM-verif16,
  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},
  booktitle = wine16,
  year   = 2016,
  pages  = {273--293},
  series = lncs,
  volume = 10123,
  publisher = springer,
  url    = {http://arxiv.org/abs/1502.04052},
  slides = {http://justinh.su/files/slides/bic.pdf},
  jh     = yes,
  plclub    = yes,
  reviewed = yes,
}

@inproceedings{BGGHS16c,
  title  = {Advanced probabilistic couplings for differential privacy},
  author = {Barthe, Gilles and
            Fong, No{\'e}mie and
            Gaboardi, Marco and
            Gr{\'e}goire, Benjamin and
            Hsu, Justin and
            Strub, {P}ierre-{Y}ves},
  booktitle = ccs16,
  year    = 2016,
  pages   = {55--67},
  url     = {https://arxiv.org/abs/1606.07143},
  jh      = yes,
  plclub    = yes,
  reviewed = yes,
  acceptance = {137/831=0.17},
  slides  = {http://justinh.su/files/slides/advanced.pdf},
}

@inproceedings{privinfer,
  title  = {Differentially private {B}ayesian programming},
  author = {Barthe, Gilles and
            Farina, Gian Pietro and
            Gaboardi, Marco and
            Gallego Arias, Emilio Jes{\'u}s and
            Gordon, Andy and
            Hsu, Justin and
            Strub, Pierre-Yves},
  booktitle = ccs16,
  year   = {2016},
  url    = {https://arxiv.org/abs/1605.00283},
  jh     = yes,
  plclub    = yes,
  reviewed = yes,
  acceptance = {137/831=0.17},
}

@inproceedings{BEFFH16,
  title  = {Synthesizing probabilistic invariants via {D}oob's decomposition},
  author = {Barthe, Gilles and
            Espitau, Thomas and
            Ferrer Fioriti, Luis Mar{\'i}a and
            Hsu, Justin},
  booktitle = cav16,
  pages     = {43--61},
  volume    = {9779},
  series  = lncs,
  year    = 2016,
  publisher = springer,
  url     = {https://arxiv.org/abs/1605.02765},
  jh      = yes,
  plclub    = yes,
  reviewed = yes,
  acceptance = {46/195=0.24},
}

@inproceedings{BGGHS16b,
  title  = {A program logic for union bounds},
  author = {Barthe, Gilles and
            Gaboardi, Marco and
            Gr{\'e}goire, Benjamin and
            Hsu, Justin and
            Strub, {P}ierre-{Y}ves},
  booktitle = icalp16,
  pages     = {107:1--107:15},
  volume    = {55},
  series    = lipics,
  year    = 2016,
  publisher = dagstuhl,
  url     = {http://arxiv.org/abs/1602.05681},
  jh      = yes,
  plclub    = yes,
  reviewed = yes,
  acceptance = {146/515=0.28},
}

@inproceedings{BGGHS16,
  title  = {Proving differential privacy via probabilistic couplings},
  author = {Barthe, Gilles and
            Gaboardi, Marco and
            Gr{\'e}goire, Benjamin and
            Hsu, Justin and
            Strub, {P}ierre-{Y}ves},
  booktitle = lics16,
  pages     = {749--758},
  year    = 2016,
  url     = {http://arxiv.org/abs/1601.05047},
  jh      = yes,
  plclub    = yes,
  reviewed = yes,
  slides  = {http://justinh.su/files/slides/approx-couplings.pdf},
}

@inproceedings{HMRRV16,
  title  = {Do prices coordinate markets?},
  author = {Hsu, Justin and
            Morgenstern, Jamie and
            Rogers, Ryan and
            Roth, Aaron and
            Vohra, Rakesh},
  booktitle = stoc16,
  pages     = {440--453},
  year    = 2016,
  url     = {http://arxiv.org/abs/1511.00925},
  jh      = yes,
  reviewed = yes,
  acceptance = {92/370=0.25},
}

@inproceedings{HHRW16,
  author    = {Hsu, Justin and
               Huang, Zhiyi and
               Roth, Aaron and
               Wu, Zhiwei Steven},
  title     = {Jointly private convex programming},
  booktitle = soda16,
  pages     = {580--599},
  year      = {2016},
  url       = {http://arxiv.org/abs/1411.0998},
  jh        = yes,
  reviewed = yes,
  slides    = {http://justinh.su/files/slides/privdude.pdf},
  acceptance = {146/527=0.28},
}

@inproceedings{BEGHSS15,
  title     = {Relational reasoning via probabilistic coupling},
  author    = {Barthe, Gilles and
               Espitau, Thomas and
               Gr{\'e}goire, Benjamin and
               Hsu, Justin and
               Stefanesco, L{\'e}o and
               Strub, {P}ierre-{Y}ves},
  booktitle = lpar15,
  pages     = {387--401},
  volume    = {9450},
  series    = lncs,
  year      = 2015,
  publisher = springer,
  url       = {http://arxiv.org/abs/1509.03476},
  jh        = yes,
  plclub    = yes,
  reviewed  = yes,
  slides    = {http://justinh.su/files/slides/couplings.pdf},
  acceptance = {43/92=0.47},
}

@inproceedings{AHJ15,
  title     = {Online assignment with heterogeneous tasks in crowdsourcing markets},
  author    = {Assadi, Sepehr and Hsu, Justin and Jabbari, Shahin},
  booktitle = hcomp15,
  pages     = {12--21},
  year      = {2015},
  url       = {http://arxiv.org/abs/1508.03593},
  jh        = yes,
  reviewed  = yes,
}

@inproceedings{GHaccuracy,
  author    = {Marco Gaboardi and
               Justin Hsu},
  title     = {A {Theory AB} toolbox},
  year      = {2015},
  booktitle = snapl15,
  pages     = {129--139},
  volume    = {32},
  series    = lipics,
  publisher = dagstuhl,
  url       = {http://justinh.su/files/papers/theory-ab.pdf},
  jh        = yes,
  plclub    = yes,
  reviewed  = yes,
  slides    = {http://justinh.su/files/slides/theory-ab.pdf},
}

@inproceedings{BGGHRS15,
  title     = {Higher-order approximate relational refinement types for
    mechanism design and differential privacy},
  author    = {Barthe, Gilles and
               Gaboardi, Marco and
               Gallego Arias, Emilio Jes{\'u}s and
               Hsu, Justin and
               Roth, Aaron and
               Strub, Pierre-Yves},
  booktitle = popl15,
  pages     = {55--68},
  year      = {2015},
  url       = {http://arxiv.org/abs/1407.6845},
  jh        = yes,
  plclub    = yes,
  reviewed  = yes,
  slides    = {http://justinh.su/files/slides/hoare2.pdf},
  acceptance = {52/227=0.23},
}

@inproceedings{AGGH14,
  author    = {de Amorim, Arthur Azevedo and
               Gaboardi, Marco and
               Gallego Arias, Emilio Jes{\'u}s and
               Hsu, Justin},
  title     = {Really natural linear indexed type-checking},
  booktitle = {Symposium on Implementation and Application of Functional
    Programming Languages (IFL), Boston, Massachusetts},
  pages     = {5:1--5:12},
  year      = {2014},
  publisher = acmpress,
  url       = {http://arxiv.org/abs/1503.04522},
  jh        = yes,
  plclub    = yes,
  reviewed  = yes,
  slides    = {http://justinh.su/files/slides/dfuzz-tc.pdf},
}

@inproceedings{BGGHKS14,
  author    = {Barthe, Gilles and
               Gaboardi, Marco and
               Gallego Arias, Emilio Jes{\'u}s and
               Hsu, Justin and
               Kunz, C\'esar and
               Strub, Pierre-Yves},
  title     = {Proving differential privacy in {H}oare logic},
  booktitle = csf14,
  pages     = {411--424},
  year      = {2014},
  url       = {http://arxiv.org/abs/1407.2988},
  jh        = yes,
  plclub    = yes,
  reviewed  = yes,
  acceptance = {29/83=0.35},
}

@inproceedings{HGH14,
  author    = {Hsu, Justin and
               Gaboardi, Marco and
               Haeberlen, Andreas and
               Khanna, Sanjeev and
               Narayan, Arjun and
               Pierce, Benjamin C. and
               Roth, Aaron},
  title     = {Differential privacy: {An} economic method for choosing epsilon},
  booktitle = csf14,
  pages     = {398--410},
  year      = 2014,
  url       = {http://arxiv.org/abs/1402.3329},
  jh        = yes,
  plclub    = yes,
  reviewed  = yes,
  slides    = {http://justinh.su/files/slides/epsilon.pdf},
  acceptance = {29/83=0.35},
}

@inproceedings{HRRU14,
  author    = {Hsu, Justin and
               Roth, Aaron and
               Roughgarden, Tim and
               Ullman, Jonathan},
  title     = {Privately solving linear programs},
  booktitle = icalp14,
  pages     = {612--624},
  volume    = 8572,
  series    = lncs,
  year      = {2014},
  publisher = springer,
  url       = {http://arxiv.org/abs/1402.3631},
  jh        = yes,
  reviewed  = yes,
  slides    = {http://justinh.su/files/slides/priv-lp.pdf},
  acceptance = {136/477=0.29},
}

inproceedings{GGHRW14,
  author    = {Gaboardi, Marco and
               Gallego Arias, Emilio Jes{\'u}s and
               Hsu, Justin and
               Roth, Aaron and
               Wu, Zhiwei Steven},
  title     = {Dual Query: Practical private query release for high dimensional data},
  booktitle = icml14,
  pages     = {1170--1178},
  volume    = {32},
  series    = jmlrproc,
  year      = {2014},
  publisher = jmlr,
  reviewed  = yes,
  url       = {http://arxiv.org/abs/1402.1526},
  jh        = yes,
  slides    = {http://justinh.su/files/slides/dualquery.pdf},
  poster    = {http://justinh.su/files/poser/dualquery.pdf},
  acceptance = {310/1238=0.25},
}

inproceedings{HHRRW14,
  author    = {Hsu, Justin and
               Huang, Zhiyi and
               Roth, Aaron and
               Roughgarden, Tim and
               Wu, Zhiwei Steven},
  title     = {Private matchings and allocations},
  booktitle = stoc14,
  year      = {2014},
  reviewed  = yes,
  pages     = {21--30},
  url       = {http://arxiv.org/abs/1311.2828},
  timestamp = {Wed, 22 Oct 2014 14:44:14 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/stoc/HsuHRRW14},
  bibsource = {dblp computer science bibliography, http://dblp.org},
  jh        = yes,
  poster    = {http://justinh.su/files/poster/matchings.pdf},
  acceptance = {91/319=0.29},
}

@inproceedings{WHE13,
  title     = {{S}ystem {FC} with explicit kind equality},
  author    = {Weirich, Stephanie and
               Hsu, Justin and
               Eisenberg, Richard A.},
  booktitle = icfp13,
  pages     = {275--286},
  year      = {2013},
  url       = {http://www.cis.upenn.edu/~justhsu/docs/nokinds.pdf},
  jh        = yes,
  plclub    = yes,
  reviewed  = yes,
  acceptance = {40/133=0.30},
}

@inproceedings{HRU13,
  title     = {Differential privacy for the analyst via private equilibrium computation},
  author    = {Hsu, Justin and
               Roth, Aaron and
               Ullman, Jonathan},
  url       = {http://arxiv.org/abs/1211.0877},
  booktitle = stoc13,
  pages     = {341--350},
  year      = {2013},
  jh        = yes,
  reviewed  = yes,
  slides    = {http://justinh.su/files/slides/analyst-priv.pdf},
  acceptance = {100/360=0.28},
}

@inproceedings{GHHNP13,
  title     = {Linear dependent types for differential privacy},
  author    = {Gaboardi, Marco and
               Haeberlen, Andreas and
               Hsu, Justin and
               Narayan, Arjun and
               Pierce, Benjamin C.},
  booktitle = popl13,
  pages     = {357--370},
  url       = {http://dl.acm.org/citation.cfm?id=2429113},
  year      = {2013},
  jh        = yes,
  plclub    = yes,
  reviewed  = yes,
  acceptance = {51/220=0.23},
}

@inproceedings{HKR12,
  title     = {Distributed private heavy hitters},
  author    = {Hsu, Justin and
               Khanna, Sanjeev and
               Roth, Aaron},
  booktitle = icalp12,
  pages     = {461--472},
  volume    = {7391},
  series    = lncs,
  year      = {2012},
  publisher = springer,
  url       = {http://arxiv.org/abs/1202.4910},
  note      = {Thanks to Raef Bassily and Adam Smith for spotting an error, now
               fixed.},
  jh        = yes,
  reviewed  = yes,
  slides    = {http://justinh.su/files/slides/heavy-hh.pdf},
  acceptance = {123/433=0.28},
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% SURVEYS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@article{Murawski:2016:2893582,
	title      = {Programming language techniques for differential privacy},
	author     = {Barthe, Gilles and
                Gaboardi, Marco and
                Hsu, Justin and
                Pierce, Benjamin C.},
	pages      = {34--53},
	journal    = {ACM SIGLOG News},
  month      = jan,
	year       = {2016},
	volume     = {3},
	number     = {1},
	url        = {http://siglog.hosting.acm.org/wp-content/uploads/2016/01/siglog_news_7.pdf},
	jh         = yes,
  plclub    = yes,
  reviewed   = no,
} 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% WORKSHOPS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@inproceedings{GGHHP13,
  title     = {Automatic sensitivity analysis using linear dependent types},
  author    = {Gaboardi, Marco and
               Gallego Arias, Emilio Jes{\'u}s and
               Haeberlen, Andreas and
               Hsu, Justin and
               Pierce, Benjamin C.},
  url       = {http://fopara2013.cs.unibo.it/paper_8.pdf},
  booktitle = fopara,
  year      = {2013},
  jh        = yes,
  plclub    = yes,
  reviewed  = no,
}

@inproceedings{HsuTaxes,
  author    = {Justin Hsu},
  title     = {Death, taxes, and formal verification (Abstract)},
  year      = {2015},
  booktitle = snapl15,
  jh        = yes,
  plclub    = yes,
  reviewed  = no,
  slides    = {http://justinh.su/files/slides/taxes.pdf},
  url       = {http://justinh.su/files/papers/taxes.pdf}
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% TALKS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@talk{wine16-talk,
  title = {Computer-aided verification in mechanism design},
  organization = wine16,
  year = 2016,
  month = dec,
  jh = yes,
}

@talk{cornell16-talk,
  title = {Approximate Probabilistic Coupling and Differential Privacy},
  organization = {Theory Seminar, Cornell University},
  year = 2016,
  month = oct,
  jh = yes,
}

@talk{ccs16-talk,
  title = {Advanced Probabilistic Couplings for Differential Privacy},
  organization = ccs16,
  year = 2016,
  month = oct,
  jh = yes,
}

@talk{psu16-talk,
  title = {Differential Privacy as an Approximate Coupling},
  organization = {Theory Seminar, Pennsylvania State University},
  year = 2016,
  month = oct,
  jh = yes,
}

@talk{cmu16-talk,
  title = {Relational reasoning via probabilistic coupling},
  organization = {Principles of Programming Seminar, Carnegie Mellon University},
  year = 2016,
  month = oct,
  jh = yes,
}

@talk{jhu16-talk,
  title = {Approximate Probabilistic Coupling and Differential Privacy},
  organization = {Theory Seminar, Johns Hopkins University},
  year = 2016,
  month = oct,
  jh = yes,
}

@talk{msrc16-talk,
  title = {Formal Verification of Randomized Algorithms},
  organization = {Constructive Security Seminar, MSR Cambridge UK},
  year = 2016,
  month = jul,
  jh = yes,
}

@talk{lics16-talk,
  title = {Proving Differential Privacy via Probabilistic Couplings},
  organization = lics16,
  year = 2016,
  month = jul,
  jh = yes,
}

@talk{tpdp16-talk,
  title = {Differential Privacy is an Approximate Probabilistic Coupling},
  organization = {Workshop on the Theory and Practice of Differential Privacy (TPDP)},
  year = 2016,
  month = jun,
  jh = yes,
}

@talk{crcs16-talk,
  title = {Differential Privacy is an Approximate Probabilistic Coupling},
  organization = {CRCS Seminar, Harvard},
  year = 2016,
  month = jun,
  jh = yes,
}

@talk{njpls16-talk,
  title = {A program logic for union bounds},
  organization = {NJ Programming Languages and Systems Seminar (NJPLS)},
  year = 2016,
  month = may,
  jh = yes,
}

@talk{uwisc16-talk,
  title = {Relational reasoning via probabilistic coupling},
  organization = {PL Seminar, University of Wisconsin},
  year = 2016,
  month = may,
  jh = yes,
}

@talk{soda16-talk,
  title = {Jointly Private Convex Programming},
  organization = soda16,
  year = 2016,
  month = jan,
  jh = yes,
}

@talk{lpar15-talk,
  title = {Relational reasoning via probabilistic coupling},
  organization = lpar15,
  year = 2015,
  month = nov,
  jh = yes,
}

@talk{nsf-sfm15-talk,
  title = {What are we measuring, anyways?},
  organization = {NSF Workshop on Formal Methods for Information Security},
  year = 2015,
  month = nov,
  jh = yes,
}

@talk{tau15-talk,
  title = {Language-based Verification for Differential Privacy},
  organization = {Tel Aviv University},
  year = 2015,
  month = nov,
  jh = yes,
}

@talk{shonan15-talk,
  title = {Language-based Verification for Differential Privacy},
  organization = {Shonan Meeting on Logic and Verification Methods in Security and
    Privacy},
  year = 2015,
  month = nov,
  jh = yes,
}

@talk{tohoku15-talk,
  title = {Relational reasoning via probabilistic coupling},
  organization = {Tohoku University},
  year = 2015,
  month = oct,
  jh = yes,
}

@talk{tit15-talk,
  title = {Jointly Private Convex Programming},
  organization = {Tokyo Institute of Technology},
  year = 2015,
  month = oct,
  jh = yes,
}

@talk{snapl15b-talk,
  title = {Death, Taxes, and Formal Verification},
  organization = snapl15,
  year = 2015,
  month = may,
  jh = yes,
}

@talk{snapl15a-talk,
  title = {A {Theory AB} Toolbox},
  organization = snapl15,
  year = 2015,
  month = may,
  jh = yes,
}

@talk{cornell15-talk,
  title = {Verifying Accuracy of Randomized Algorithms},
  organization = {Cornell PL Discussion Group},
  year = 2015,
  month = mar,
  jh = yes,
}


@talk{popl15-talk,
  title = {Higher-Order Relational Refinement Types for Mechanism Design and Differential Privacy},
  organization = popl15,
  year = 2015,
  month = jan,
  jh = yes,
}

@talk{lix14-talk,
  title = {Jointly Private Convex Programming},
  organization = {Com\`ete-Parsifal Seminar, {LIX}, \'Ecole Polytechnique},
  year = 2014,
  month = nov,
  jh = yes,
}

@talk{dundee14-talk,
  title = {Jointly Private Convex Programming},
  organization = {University of Dundee},
  year = 2014,
  month = nov,
  jh = yes,
}

@talk{csf14-talk,
  title = {Differential Privacy: {An} Economic Method for Choosing Epsilon},
  organization = csf14,
  year = 2014,
  month = jul,
  jh = yes,
}

@talk{icalp14-talk,
  title = {Privately Solving Linear Programs},
  organization = icalp14,
  year = 2014,
  month = jul,
  jh = yes,
}

@talk{simons13-talk,
  title = {Dual Query Release},
  organization = {Simons workshop on Big Data and Differential Privacy},
  year = 2013,
  month = dec,
  jh = yes,
}

@talk{lix13-talk,
  title = {Private Matchings and Allocations},
  organization = {Com\`ete-Parsifal Seminar, {LIX}, \'Ecole Polytechnique},
  year = 2013,
  month = dec,
  jh = yes,
}

@talk{stoc13-talk,
  title = {Private Equilibrium Computation for Analyst Privacy},
  organization = stoc13,
  year = 2013,
  month = jun,
  jh = yes,
}

@talk{dimacs12-talk,
  title = {Analyst Privacy---the State Strikes Back!},
  organization = {{DIMACS} Workshop on Recent Work on Differential Privacy across Computer Science},
  year = 2012,
  month = oct,
  jh = yes,
}

@talk{icalp12-talk,
  title = {Distributed Private Heavy Hitters},
  organization = icalp12,
  year = 2012,
  month = jul,
  jh = yes,
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% OTHER %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

@article{job-matching,
  title   = {Job Matching, Coalition Formation, and Gross Substitutes},
  volume  = {50},
  number  = {6},
  urldate = {2013--07--07},
  journal = {Econometrica},
  author  = {Kelso, Alexander and Crawford, Vincent},
  year    = {1982},
  pages   = {1483--1504},
  url     = {http://EconPapers.repec.org/RePEc:ecm:emetrp:v:50:y:1982:i:6:p:1483-1504}
}                  
@article{CSS10,
  title   = {Private and continual release of statistics},
  volume  = {14},
  url     = {http://eprint.iacr.org/2010/076.pdf},
  number  = {3},
  urldate = {2013--06--23},
  journal = tissec,
  author  = {Chan, T.-H. Hubert and Shi, Elaine and Song, Dawn},
  year    = {2011},
  pages   = {26},
}

@inproceedings{DNPR10,
  title     = {Differential privacy under continual observation},
  author    = {Dwork, Cynthia and Naor, Moni and Pitassi, Toniann and Rothblum, Guy N.},
  url       = {http://www.mit.edu/~rothblum/papers/continalobs.pdf},
  booktitle = stoc10,
  pages     = {715--724},
  year      = {2010},
}

@inproceedings{DNV12,
  title     = {The privacy of the analyst and the power of the state},
  author    = {Dwork, Cynthia and Naor, Moni and Vadhan, Salil},
  booktitle = focs12,
  pages     = {400--409},
  url       = {http://projects.iq.harvard.edu/files/privacytools/files/06375318.pdf},
  year      = {2012}
}

@article{PR13,
  title   = {Privacy and Mechanism Design},
  author  = {Pai, Mallesh and Roth, Aaron},
  url     = {http://arxiv.org/abs/1306.2083},
  journal = sigecom,
  year    = {2013}
}

@inproceedings{NRS07,
  title     = {Smooth sensitivity and sampling in private data analysis},
  url       = {http://www.cse.psu.edu/~asmith/pubs/NRS07/NRS07-full-draft-v1.pdf},
  author    = {Nissim, Kobbi and Raskhodnikova, Sofya and Smith, Adam},
  booktitle = stoc07,
  pages     = {75--84},
  year      = {2007},
}

@inproceedings{RR14,
  title     = {Asymptotically truthful equilibrium selection in large congestion games},
  author    = {Rogers, Ryan and Roth, Aaron},
  booktitle = ec14,
  pages     = {771--782},
  year      = {2014},
  url       = {http://arxiv.org/abs/1311.2625}
}

@inproceedings{GLMRT10,
  title     = {Differentially private combinatorial optimization},
  url       = {http://arxiv.org/abs/0903.4510},
  author    = {Gupta, Anupam and Ligett, Katrina and Mc{S}herry, Frank and Roth,
    Aaron and Talwar, Kunal},
  booktitle = soda10,
  pages     = {1106--1125},
  year      = {2010},
}

@article{GS99,
  title     = {Walrasian equilibrium with gross substitutes},
  author    = {Gul, Faruk and Stacchetti, Ennio},
  url       = {http://www.princeton.edu/~fgul/walras.pdf},
  journal   = jet,
  volume    = {87},
  number    = {1},
  pages     = {95--124},
  year      = {1999},
  publisher = elsevier
}

@article{BLR08,
  title   = {A learning theory approach to noninteractive database privacy},
  author  = {Blum, Avrim and Ligett, Katrina and Roth, Aaron},
  journal = jacm,
  url     = {http://arxiv.org/abs/1109.2229},
  volume  = {60},
  number  = {2},
  pages   = {12},
  year    = {2013},
}

@inproceedings{HR10,
  title     = {A multiplicative weights mechanism for privacy-preserving data analysis},
  author    = {Hardt, Moritz and Rothblum, Guy N},
  url       = {http://www.mit.edu/~rothblum/papers/pmw.pdf},
  booktitle = focs10,
  pages     = {61--70},
  year      = {2010},
}

@inproceedings{DN03,
  title     = {Revealing information while preserving privacy},
  author    = {Dinur, Irit and Nissim, Kobbi},
  url       = {http://www.cse.psu.edu/~asmith/privacy598/papers/dn03.pdf},
  booktitle = pods03,
  pages     = {202--210},
  year      = {2003},
}

@article{DR14,
  author    = {Cynthia Dwork and
               Aaron Roth},
  title     = {The Algorithmic Foundations of Differential Privacy},
  journal   = {Foundations and Trends in Theoretical Computer Science},
  year      = {2014},
  volume    = {9},
  number    = {3--4},
  pages     = {211--407},
  url       = {http://dx.doi.org/10.1561/0400000042},
  timestamp = {Tue, 28 Oct 2014 14:00:24 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/fttcs/DworkR14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{KPRU14,
  title     = {Mechanism Design in Large Games: Incentives and Privacy},
  url       = {http://arxiv.org/abs/1207.4084},
  author    = {Kearns, Michael and Pai, Mallesh and Roth, Aaron and Ullman, Jonathan},
  pages     = {403--410},
  booktitle = itcs14,
  year      = {2014}
}

@inproceedings{DRV10,
	title     = {Boosting and differential privacy},
	url       = {http://research.microsoft.com/pubs/155170/dworkrv10.pdf},
	booktitle = focs10,
	author    = {Dwork, Cynthia and Rothblum, Guy N. and Vadhan, Salil},
	year      = {2010},
	keywords  = {Algorithms, {CS}, {DP}, Learning Theory},
	pages     = {51--60},
}

@inproceedings{FPT04,
  title     = {The complexity of pure Nash equilibria},
  author    = {Fabrikant, Alex and Papadimitriou, Christos and Talwar, Kunal},
  url       = {http://research.microsoft.com/pubs/74349/pub10-pure.pdf},
  booktitle = stoc04,
  pages     = {604--612},
  year      = {2004},
}

@article{MS96,
  title     = {Potential games},
  author    = {Monderer, Dov and Shapley, Lloyd S.},
  journal   = geb,
  url       = {http://www.cs.bu.edu/~steng/teaching/Fall2008/potential.pdf},
  volume    = {14},
  number    = {1},
  pages     = {124--143},
  year      = {1996},
  publisher = {Elsevier}
}

@inproceedings{CK05,
  title     = {The price of anarchy of finite congestion games},
  author    = {Christodoulou, George and Koutsoupias, Elias},
  url       = {http://dl.acm.org/citation.cfm?id=1060600},
  booktitle = stoc05,
  pages     = {67--73},
  year      = {2005},
}

@inproceedings{AAE05,
  title     = {The price of routing unsplittable flow},
  author    = {Awerbuch, Baruch and Azar, Yossi and Epstein, Amir},
  booktitle = stoc05,
  url       = {http://dl.acm.org/citation.cfm?id=1060599},
  pages     = {57--66},
  year      = {2005},
}

@inproceedings{Rou09,
  title     = {Intrinsic robustness of the price of anarchy},
  author    = {Roughgarden, Tim},
  url       = {http://theory.stanford.edu/~tim/papers/robust.pdf},
  booktitle = stoc09,
  pages     = {513--522},
  year      = {2009},
}

@inproceedings{BHLR08,
  title     = {Regret minimization and the price of total anarchy},
  author    = {Blum, Avrim and {HajiAghayi}, {MohammadTaghi} and Ligett, Katrina
    and Roth, Aaron},
  url       = {http://dl.acm.org/citation.cfm?id=1374430},
  booktitle = stoc08,
  pages     = {373--382},
  year      = {2008},
}

@inproceedings{HLM12,
  title     = {A Simple and Practical Algorithm for Differentially Private Data Release},
  author    = {Moritz Hardt and Katrina Ligett and Frank {McSherry}},
  booktitle = nips12,
  pages     = {2348--2356},
  url       = {http://arxiv.org/abs/1012.4763},
  year      = 2012
}

@inproceedings{Ullman13,
  title     = {Answering $n^{2+ o(1)}$ counting queries with differential
    privacy is hard},
  author    = {Ullman, Jonathan},
  booktitle = stoc13,
  pages     = {361--370},
  url       = {http://arxiv.org/abs/1207.6945},
  year      = 2013
}
@inproceedings{MT07,
  author    = {Frank {McSherry} and
               Kunal Talwar},
  title     = {Mechanism Design via Differential Privacy},
  booktitle = focs07,
  pages     = {94--103},
  url       = {http://doi.ieeecomputersociety.org/10.1109/FOCS.2007.41},
  year      = 2007
}

@inproceedings{FS96,
  title     = {Game theory, on-line prediction and boosting},
  author    = {Freund, Y. and Schapire, R.E.},
  booktitle = colt96,
  pages     = {325--332},
  url       = {http://dl.acm.org/citation.cfm?id=238163 },
  year      = 1996
}

@inproceedings{BDMN05,
  title     = {Practical privacy: the {SuLQ} framework},
  author    = {Avrim Blum and
               Cynthia Dwork and
               Frank Mc{S}herry and
               Kobbi Nissim},
  booktitle = pods05,
  pages     = {128--138},
  url       = {http://research.microsoft.com/pubs/64351/bdmn.pdf},
  year      = 2005
}

@inproceedings{GRU12,
  title     = {Iterative constructions and private data release},
  author    = {Gupta, Anupam and Roth, Aaron and Jonathan Ullman},
  booktitle = tcc12,
  pages     = {339--356},
  url       = {http://arxiv.org/abs/1107.3731},
  year      = 2012
}

@inproceedings{airavat,
  author       = {Indrajit Roy and Srinath Setty and Ann Kilzer and Vitaly
    Shmatikov and Emmett Witchel},
  title        = {Airavat: Security and Privacy for {MapReduce}},
  booktitle    = nsdi10,
  url          = {http://dl.acm.org/citation.cfm?id=1855731 },
  year         = 2010
}

@inproceedings{pinq,
  author       = {{McSherry}, Frank},
  booktitle    = sigmod09,
  title        = {Privacy integrated queries},
  pages        = {19--30},
  url          = {http://research.microsoft.com/pubs/80218/sigmod115-mcsherry.pdf},
  year         = 2009
}

@inproceedings{zhang-2011-privatemining,
  author       = {Zhang, Ning and Li, Ming and Lou, Wenjing},
  title        = {Distributed Data Mining with Differential Privacy},
  booktitle    = icc11,
  url          = {http://dl.acm.org/citation.cfm?id=1835868},
  year         = 2011
}

@inproceedings{evfimievski-2002-associationrules,
 author        = {Evfimievski, Alexandre and
                  Srikant, Ramakrishnan and
                  Agrawal, Rakesh and
                  Gehrke, Johannes},
 title         = {Privacy preserving mining of association rules},
 booktitle     = kdd02,
 url           = {http://www.cs.cornell.edu/johannes/papers/2002/kdd2002-privacy.pdf},
 year          = 2002
} 

@inproceedings{t-closeness,
  author       = {Ninghui Li and Tiancheng Li and Suresh Venkatasubramanian},
  title        = {$t$-{C}loseness: {P}rivacy beyond $k$-anonymity and $l$-diversity},
  booktitle    = icde07,
  url          = {https://www.cs.purdue.edu/homes/ninghui/papers/t_closeness_icde07.pdf},
  year         = 2007
}

@article{k-anonymity,
 author        = {Sweeney, Latanya},
 title         = {$k$-{Anonymity}: {A} model for protecting privacy},
 journal       = jufks,
 volume        = {10},
 number        = {5},
 year          = {2002},
 pages         = {557--570},
 url           = {http://dl.acm.org/citation.cfm?id=774552}
} 

@article{aol,
  author       = {Michael Barbaro and Tom Zeller},
  title        = {A Face Is Exposed for {AOL} Searcher {N}o. 4417749},
  journal      = {The New York Times},
  day          = 9,
  month        = aug,
  year         = 2006,
  url          = {http://www.nytimes.com/2006/08/09/technology/09aol.html}
}

@inproceedings{NV08,
  author       = {Arvind Narayanan and
               Vitaly Shmatikov},
  title        = {Robust De-anonymization of Large Sparse Datasets},
  booktitle    = sp08,
  year         = {2008},
  pages        = {111--125},
  url          = {http://arxiv.org/abs/cs/0610105}
}

@inproceedings{BLST10,
  author       = {Raghav Bhaskar and
                  Srivatsan Laxman and
                  Adam Smith and
                  Abhradeep Thakurta},
  title        = {Discovering frequent patterns in sensitive data},
  booktitle    = kdd10,
  pages        = {503--512},
  year         = 2010,
  url          = {http://dl.acm.org/citation.cfm?id=1835869}
}

@inproceedings{CM08,
  author       = {Kamalika Chaudhuri and Claire Monteleoni},
  title        = {Privacy-preserving logistic regression},
  booktitle    = nips08,
  pages        = {289--296},
  year         = 2008,
  url          = {http://books.nips.cc/papers/files/nips21/NIPS2008_0964.pdf}
}

@article{CH11,
  title        = {Sample Complexity Bounds for Differentially Private Learning},
  author       = {Chaudhuri, Kamalika and Hsu, Daniel},
  journal      = jmlr,
  volume       = {19},
  pages        = {155--186},
  url          = {http://jmlr.org/proceedings/papers/v19/chaudhuri11a/chaudhuri11a.pdf},
  year         = {2011}
}

@article{BKOZ13-toplas,
  author       = {Barthe, Gilles and
                  K{\"{o}}pf, Boris and
                  Olmedo, Federico and
                  Zanella{-}B{\'{e}}guelin, Santiago},
  title        = {Probabilistic Relational Reasoning for Differential Privacy},
  journal      = toplas,
  volume       = {35},
  number       = {3},
  pages        = {9:1--9:49},
  month        = nov,
  year         = {2013},
  url          = {http://software.imdea.org/~bkoepf/papers/toplas13.pdf},
}

@inproceedings{ReedPierce10,
  author       = {Jason Reed and Benjamin C. Pierce},
  title        = {Distance Makes the Types Grow Stronger: {A} Calculus for
    Differential Privacy},
  booktitle    = icfp10,
  year         = 2010,
  pages        = {157--168},
  url          = {http://dl.acm.org/citation.cfm?id=1863568}
}

@inproceedings{winq,
  title        = {A workflow for differentially-private graph synthesis},
  author       = {Proserpio, Davide and Goldberg, Sharon and {McSherry}, Frank},
  booktitle    = wosn12,
  year         = 2012,
  pages        = {13--18},
  url          = {http://arxiv.org/abs/1203.3453}
}

@article{KLNRS08,
  title        = {What can we learn privately?},
  author       = {Kasiviswanathan, Shiva Prasad and Lee, Homin K. and Nissim, Kobbi
    and Raskhodnikova, Sofya and Smith, Adam},
  journal      = siamjc,
  volume       = {40},
  number       = {3},
  pages        = {793--826},
  year         = {2011},
  url          = {http://arxiv.org/abs/0803.0924},
}

@inproceedings{UV11,
  title        = {{PCPs} and the hardness of generating private synthetic data},
  author       = {Ullman, Jonathan and Vadhan, Salil},
  booktitle    = tcc11,
  pages        = {400--416},
  url          = {http://eccc.hpi-web.de/report/2010/017/revision/2/download},
  year         = {2011}
}

@inproceedings{DNRRV09,
  title        = {On the complexity of differentially private data release: efficient
    algorithms and hardness results},
  author       = {Cynthia Dwork and
                  Moni Naor and
                  Omer Reingold and
                  Guy N. Rothblum and
                  Salil P. Vadhan},
  booktitle    = stoc09,
  pages        = {381--390},
  year         = {2009},
  url          = {http://dl.acm.org/citation.cfm?id=1536467}
}

@article{AHK12,
  title        = {The Multiplicative Weights Update Method: {A} Meta-Algorithm and
    Applications},
  author       = {Arora, Sanjeev and Hazan, Elad and Kale, Satyen},
  journal      = toc,
  volume       = {8},
  number       = {1},
  pages        = {121--164},
  url          = {http://tocbeta.cs.uchicago.edu/articles/v008a006/v008a006.pdf},
  year         = {2012}
}

@phdthesis{Garg13,
  title        = {Candidate Multilinear Maps},
  author       = {Sanjam Garg},
  school       = {{UCLA}},
  year         = {2013},
  url          = {http://www.cs.ucla.edu/~sanjamg/Sanjam%20Garg_files/sanjam-thesis.pdf}
}

@inproceedings{GargGentryHalevi13,
  title        = {Candidate multilinear maps from ideal lattices},
  author       = {Garg, Sanjam and Gentry, Craig and Halevi, Shai},
  booktitle    = eucrypt13,
  pages        = {1--17},
  year         = {2013},
  url          = {http://http://eprint.iacr.org/2012/610.pdf}
}

@article{BonehSilverberg03,
  title        = {Applications of multilinear forms to cryptography},
  author       = {Boneh, Dan and Silverberg, Alice},
  journal      = {Contemporary Mathematics},
  volume       = {324},
  number       = {1},
  pages        = {71--90},
  year         = {2003},
  publisher    = {AMS},
  url          = {http://https://eprint.iacr.org/2002/080.pdf}
}

@inproceedings{barak2007privacy,
  title        = {Privacy, accuracy, and consistency too: {A} holistic solution to
    contingency table release},
  author       = {Barak, Boaz and Chaudhuri, Kamalika and Dwork, Cynthia and Kale,
    Satyen and Mc{S}herry, Frank and Talwar, Kunal},
  booktitle    = pods07,
  pages        = {273--282},
  url          = {http://research.microsoft.com/en-us/projects/DatabasePrivacy/contingency.pdf},
  year         = {2007}
}

@inproceedings{BNS13,
  title        = {Characterizing the sample complexity of private learners},
  author       = {Beimel, Amos and Nissim, Kobbi and Stemmer, Uri},
  booktitle    = itcs13,
  pages        = {97--110},
  year         = {2013},
  url          = {http://dl.acm.org/citation.cfm?id=2422450}
}

@article{CMS11,
  title        = {Differentially private empirical risk minimization},
  author       = {Chaudhuri, Kamalika and Monteleoni, Claire and Sarwate, Anand D.},
  journal      = jmlr,
  volume       = {12},
  pages        = {1069--1109},
  year         = {2011},
  url          = {http://jmlr.org/papers/volume12/chaudhuri11a/chaudhuri11a.pdf}
}

@article{RBHT09,
  title        = {Learning in a Large Function Space: Privacy-Preserving Mechanisms
    for {SVM} Learning},
  author       = {Rubinstein, Benjamin I. P. and Bartlett, Peter L. and Huang, Ling
    and Taft, Nina},
  journal      = jpc,
  volume       = {4},
  number       = {1},
  pages        = {4},
  year         = {2012},
  url          = {http://repository.cmu.edu/cgi/viewcontent.cgi?article=1065&context=jpc}
}

@article{KST12,
  title        = {Private convex empirical risk minimization and high-dimensional regression},
  author       = {Kifer, Daniel and Smith, Adam and Thakurta, Abhradeep},
  journal      = jmlr,
  volume       = {1},
  pages        = {41},
  year         = {2012},
  url          = {http://jmlr.org/proceedings/papers/v23/kifer12/kifer12.pdf}
}

@inproceedings{CSS12,
  title        = {Near-optimal differentially private principal components},
  author       = {Chaudhuri, Kamalika and Sarwate, Anand and Sinha, Kaushik},
  booktitle    = nips12,
  pages        = {998--1006},
  url          = {http://books.nips.cc/papers/files/nips25/NIPS2012_0482.pdf},
  year         = {2012}
}

@inproceedings{DJW13,
  title        = {Local privacy and statistical minimax rates},
  author       = {Duchi, John C and Jordan, Michael I. and Wainwright, Martin J.},
  booktitle    = focs13,
  url          = {http://www.cs.berkeley.edu/~jduchi/projects/DuchiJoWa13_focs.pdf},
  year         = {2013}
}

@inproceedings{TS13,
  title        = {(Nearly) Optimal Algorithms for Private Online Learning in
    Full-information and Bandit Settings},
  author       = {Thakurta, Abhradeep G. and Smith, Adam},
  booktitle    = nips13,
  pages        = {2733--2741},
  url          = {http://media.nips.cc/nipsbooks/nipspapers/paper_files/nips26/1270.pdf},
  year         = {2013}
}

@inproceedings{FS95,
  title        = {A desicion-theoretic generalization of on-line learning and an
    application to boosting},
  author       = {Freund, Yoav and Schapire, Robert E.},
  booktitle    = colt95,
  pages        = {23--37},
  year         = {1995},
  organization = springer
}

@inproceedings{RR10,
  author       = {Aaron Roth and
               Tim Roughgarden},
  title        = {Interactive privacy via the median mechanism},
  booktitle    = stoc10,
  pages        = {765--774},
  url          = {http://arxiv.org/abs/0911.1813},
  year         = 2010
}

@inproceedings{GHRU11,
  title        = {Privately releasing conjunctions and the statistical query barrier},
  author       = {Gupta, Anupam and Hardt, Moritz and Roth, Aaron and Ullman, Jonathan},
  booktitle    = stoc11,
  pages        = {803--812},
  url          = {http://arxiv.org/abs/1011.1296},
  year         = {2011}
}

@inproceedings{TS13a,
  title        = {Differentially Private Feature Selection via Stability Arguments,
    and the Robustness of the Lasso},
  author       = {Thakurta, Abhradeep G. and Smith, Adam},
  booktitle    = colt13,
  pages        = {819--850},
  url          = {http://jmlr.org/proceedings/papers/v30/Guha13.pdf},
  year         = {2013}
}

@inproceedings{DL09,
  title        = {Differential privacy and robust statistics},
  author       = {Dwork, Cynthia and Lei, Jing},
  booktitle    = stoc09,
  pages        = {371--380},
  year         = {2009},
  url          = {http://research.microsoft.com/pubs/80239/dl09.pdf},
}

@article{LW94,
  title        = {The Weighted Majority Algorithm},
  author       = {Littlestone, N. and Warmuth, Manfred K.},
  journal      = ic,
  volume       = {108},
  number       = {2},
  pages        = {212--261},
  year         = {1994},
  publisher    = elsevier,
  url          = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber = 63487}
}

@article{PST95,
  title        = {Fast approximation algorithms for fractional packing and covering
    problems},
  author       = {Plotkin, Serge A. and Shmoys, David B. and Tardos, {\'E}va},
  journal      = mor,
  volume       = {20},
  number       = {2},
  pages        = {257--301},
  year         = {1995},
  publisher    = informs,
}

@inproceedings{AK07,
  title        = {A combinatorial, primal-dual approach to semidefinite programs},
  author       = {Arora, Sanjeev and Kale, Satyen},
  booktitle    = stoc07,
  pages        = {227--236},
  year         = {2007},
  url          = {http://dl.acm.org/citation.cfm?id=1250823}
}

@inproceedings{CHRMM10,
  title        = {Optimizing linear counting queries under differential privacy},
  author       = {Li, Chao and Hay, Michael and Rastogi, Vibhor and Miklau, Gerome
    and Mc{G}regor, Andrew},
  booktitle    = pods10,
  pages        = {123--134},
  year         = {2010},
  url          = {http://arxiv.org/abs/0912.4742}
}

@inproceedings{LM12,
  title        = {An adaptive mechanism for accurate query answering under differential privacy},
  author       = {Li, Chao and Miklau, Gerome},
  booktitle    = vldb12,
  volume       = {5},
  number       = {6},
  pages        = {514--525},
  year         = {2012},
  url          = {http://arxiv.org/abs/1202.3807}
}


@inproceedings{CPSY12,
  author       = {Grigory Yaroslavtsev and
               Graham Cormode and
               Cecilia M. Procopiuc and
               Divesh Srivastava},
  title        = {Accurate and efficient private release of datacubes and
    contingency tables},
  booktitle    = icde13,
  year         = {2013},
  pages        = {745--756},
  url          = {http://doi.ieeecomputersociety.org/10.1109/ICDE.2013.6544871}
}

@inproceedings{CV13,
  title     = {A Stability-based Validation Procedure for Differentially Private
    Machine Learning},
  author    = {Chaudhuri, Kamalika and Vinterbo, Staal A.},
  booktitle = nips13,
  pages     = {2652--2660},
  year      = {2013},
  url       = {http://papers.nips.cc/paper/5014-a-stability-based-validation-procedure-for-differentially-private-machine-learning.pdf}
}

@article{HW01,
  title   = {Tracking the best linear predictor},
  author  = {Herbster, Mark and Warmuth, Manfred K.},
  journal = jmlr,
  volume  = {1},
  pages   = {281--309},
  url     = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.90.7354&rep=rep1&type=pdf},
  year    = {2001}
}

@inproceedings{DworkSurvey,
  title     = {Differential privacy: {A} survey of results},
  author    = {Dwork, Cynthia},
  booktitle = tamc08,
  pages     = {1--19},
  year      = {2008},
  url       = {http://research.microsoft.com/apps/pubs/default.aspx?id=74339},
  publisher = springer
}

@inproceedings{NS-social,
  title     = {De-anonymizing social networks},
  author    = {Narayanan, Arvind and Shmatikov, Vitaly},
  booktitle = sp09,
  pages     = {173--187},
  url       = {http://arxiv.org/abs/0903.3276},
  year      = {2009}
}

@inproceedings{DNT14,
  title     = {Using Convex Relaxations for Efficiently and Privately Releasing
    Marginals},
  author    = {Dwork, Cynthia and Nikolov, Aleksandar and Talwar, Kunal},
  booktitle = socg14,
  pages     = {261},
  year      = {2014},
  url       = {http://arxiv.org/abs/1308.1385}
}

@inproceedings{TUV12,
  title     = {Faster algorithms for privately releasing marginals},
  author    = {Thaler, Justin and Ullman, Jonathan and Vadhan, Salil},
  booktitle = icalp12,
  pages     = {810--821},
  year      = {2012},
  url       = {http://arxiv.org/abs/1205.1758}
}

@article{GHRU13,
  title     = {Privately releasing conjunctions and the statistical query barrier},
  author    = {Gupta, Anupam and Hardt, Moritz and Roth, Aaron and Ullman,
    Jonathan},
  journal   = siamjc,
  volume    = {42},
  number    = {4},
  pages     = {1494--1520},
  year      = {2013},
  url       = {http://epubs.siam.org/doi/abs/10.1137/110857714}
}

@inproceedings{DunfieldP04,
  author    = {Joshua Dunfield and
               Frank Pfenning},
  title     = {Tridirectional typechecking},
  booktitle = popl04,
  pages     = {281--292},
  year      = 2004,
  url       = {http://www.cs.cmu.edu/~joshuad/papers/tridirectional-typechecking/Dunfield04_tridirectional.pdf}
}


@article{Meyer92,
  title     = {Applying ``{D}esign by contract''},
  author    = {Meyer, Bertrand},
  journal   = {Computer},
  volume    = {25},
  number    = {10},
  pages     = {40--51},
  year      = {1992},
  publisher = {IEEE},
  url       = {http://www-public.int-evry.fr/~gibson/Teaching/CSC7322/ReadingMaterial/Meyer92.pdf}
}

@inproceedings{Vazou+14:ICFP,
author    = {N. Vazou and E. L. Seidel and R. Jhala and D. Vytiniotis and
                  S. {P}eyton-{J}ones},
title     = {{Refinement Types for Haskell}},
booktitle = icfp14,
year      = {2014},
url       = {http://goto.ucsd.edu/~nvazou/refinement_types_for_haskell.pdf}
}

@inproceedings{NR99,
  title     = {Algorithmic mechanism design},
  author    = {Nisan, Noam and Ronen, Amir},
  booktitle = stoc99,
  pages     = {129--140},
  year      = {1999},
  url       = {http://www.cs.yale.edu/homes/jf/nisan-ronen.pdf}
}

@book{NRTV07,
  title     = {Algorithmic game theory},
  author    = {Nisan, Noam and Roughgarden, Tim and Tardos, Eva and Vazirani, Vijay V},
  year      = {2007},
  publisher = cup
}

@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}
}

@inproceedings{DD09,
  title     = {On the power of randomization in algorithmic mechanism design},
  author    = {Dobzinski, Shahar and Dughmi, Shaddin},
  booktitle = focs09,
  pages     = {505--514},
  url       = {http://arxiv.org/abs/0904.4193}
}

@article{DugR14,
  title   = {Black-box randomized reductions in algorithmic mechanism design},
  author  = {Dughmi, Shaddin and Roughgarden, Tim},
  journal = siamjc,
  volume  = {43},
  number  = {1},
  pages   = {312--336},
  year    = {2014},
  url     = {http://theory.stanford.edu/~tim/papers/blackbox.pdf}
}

@inproceedings{CIL12,
  title     = {On the limits of black-box reductions in mechanism design},
  author    = {Chawla, Shuchi and Immorlica, Nicole and Lucier, Brendan},
  booktitle = stoc12,
  year      = {2012},
  url       = {http://arxiv.org/abs/1109.2067}
}

@inproceedings{HL10,
  title     = {Bayesian algorithmic mechanism design},
  author    = {Hartline, Jason D and Lucier, Brendan},
  booktitle = stoc10,
  pages     = {301--310},
  year      = {2010},
  url       = {http://arxiv.org/abs/0909.4756}
}

@inproceedings{Ramsey:2002,
	Author    = {Ramsey, Norman and Pfeffer, Avi},
	Booktitle = popl02,
	Pages     = {154--165},
	Title     = {Stochastic lambda calculus and monads of probability distributions},
	Year      = {2002},
  url       = {http://www.cs.tufts.edu/~nr/pubs/pmonad.pdf}
}


@inproceedings{Park:2005,
  author    = {Sungwoo Park and
               Frank Pfenning and
               Sebastian Thrun},
  title     = {A probabilistic language based upon sampling functions},
  booktitle = popl05,
  year      = {2005},
  pages     = {171--182},
  url       = {https://www.cs.cmu.edu/~fp/papers/popl05.pdf}
}

@article{Hurd:2005,
	Author    = {Hurd, Joe and {M}c{I}ver, Annabelle and Morgan, Carroll},
	Journal   = tcs,
	Number    = {1},
	Pages     = {96--112},
	Title     = {Probabilistic guarded commands mechanized in {HOL}},
	Volume    = {346},
	Year      = {2005},
  url       = {http://www.cse.unsw.edu.au/~carrollm/probs/Papers/Hurd-05.pdf}
}

@book{McIver:2005,
	Author    = {{M}c{I}ver, A. and Morgan, C.},
	Publisher = springer,
	Series    = {Monographs in Computer Science},
	Title     = {Abstraction, Refinement, and Proof for Probabilistic Systems},
	Year      = {2005}}

@inproceedings{Borgstrom:2011,
  author    = {Johannes Borgstr{\"o}m and
               Andrew D Gordon and
               Michael Greenberg and
               James Margetson and
               Jurgen Van Gael},
  title     = {Measure Transformer Semantics for Bayesian Machine Learning},
  booktitle = esop11,
  year      = {2011},
  pages     = {77--96},
  url       = {http://cis.upenn.edu/~mgree/papers/esop2011_mts.pdf}
}

@inproceedings{Kiselyov:2009,
  author    = {Oleg Kiselyov and
               {C}hung-{C}hieh Shan},
  title     = {Embedded Probabilistic Programming},
  booktitle = {DSL},
  year      = {2009},
  pages     = {360--384}
}

@inproceedings{Goodman:2013,
  author    = {Noah D Goodman},
  title     = {The principles and practice of probabilistic programming},
  booktitle = popl13,
  year      = {2013},
  pages     = {399--402},
  url       = {https://web.stanford.edu/~ngoodman/papers/POPL2013-abstract.pdf}
}

@inproceedings{Sampson+14,
  title     = {Expressing and verifying probabilistic assertions},
  author    = {Sampson, Adrian and Panchekha, Pavel and Mytkowicz, Todd and {M}c{K}inley, Kathryn S and Grossman, Dan and Ceze, Luis},
  booktitle = pldi14,
  pages     = {14},
  year      = {2014},
  url       = {http://research.microsoft.com/pubs/211410/passert-pldi2014.pdf}
}

@Inproceedings {Bornholt+14,
author      = {James Bornholt and Todd Mytkowicz and Kathryn S {M}c{K|inley}},
booktitle   = asplos14,
title       = {{Uncertain$\langle$T$\rangle$}: {A} First-Order Type for Uncertain Data},
year        = {2014},
url         = {http://research.microsoft.com/pubs/208236/asplos077-bornholtA.pdf}
}


@article{Giry82,
    author  = {Giry, Mich\`{e}le},
    journal = {Categorical Aspects of Topology and Analysis},
    pages   = {68--85},
    title   = {{A categorical approach to probability theory}},
    year    = {1982},
}


@inproceedings{FreemanP91,
  title     = {Refinement types for {ML}},
  author    = {Freeman, Tim and Pfenning, Frank},
  booktitle = pldi91,
  pages     = {268--277},
  year      = {1991},
  url       = {https://www.cs.cmu.edu/~fp/papers/pldi91.pdf}
}

@inproceedings{BBFGM08,
  author    = "J. Bengtson and K. Bhargavan and C. Fournet and A. D. Gordon and S. Maffeis",
  title     = "Refinement types for secure implementations",
  booktitle = csf08,
  year      = 2008,
  url       = {http://prosecco.gforge.inria.fr/personal/karthik/pubs/refinement-types-for-secure-implementations-proceedings-csf08.pdf}
}


@inproceedings{fstar,
 author    = {Swamy, Nikhil and Chen, Juan and Fournet, C{\'e}dric and Strub, {P}ierre-{Y}ves and Bhargavan, Karthikeyan and Yang, Jean},
 title     = {Secure distributed programming with value-dependent types},
 booktitle = icfp11,
 year      = 2011,
 url       = {http://research.microsoft.com/pubs/150012/icfp-camera-ready.pdf}
}


@inproceedings{liquid,
  title     = {Liquid types},
  author    = {Rondon, Patrick M and Kawaguci, Ming and Jhala, Ranjit},
  booktitle = pldi08,
  pages     = {159--169},
  year      = {2008},
  url       = {http://goto.ucsd.edu/~rjhala/papers/liquid_types.pdf}
}

@inproceedings{rfstar,
  title     = {Probabilistic relational verification for cryptographic implementations},
  author    = {Barthe, Gilles and
               Fournet, C{\'e}dric and
               Gr{\'e}goire, Benjamin and
               Strub, {P}ierre-{Y}ves and
               Swamy, Nikhil and
               Zanella{-}B{\'e}guelin, Santiago},
  booktitle = popl14,
  pages     = {193--206},
  year      = {2014},
  url       = {http://research.microsoft.com/en-us/um/people/nswamy/papers/rfstar.pdf}
}

@INPROCEEDINGS{polymonad,
  TITLE     = {Polymonadic Programming},
  AUTHOR    = {Michael Hicks and Gavin Bierman and Nataliya Guts and Daan Leijen and Nikhil Swamy},
  BOOKTITLE = mfps14,
  YEAR      = 2014,
  url       = {http://arxiv.org/abs/1406.2060}
}


@inproceedings{Dwork06,
	Author       = {Dwork, Cynthia},
	Booktitle    = icalp06,
	Pages        = {1--12},
	Title        = {Differential Privacy},
	Year         = {2006},
  url          = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.83.7534&rep=rep1&type=pdf}
}

@inproceedings{Benton04,
	Author       = {Benton, Nick},
	Booktitle    = popl04,
	Pages        = {14--25},
	Title        = {Simple relational correctness proofs for static analyses and program transformations},
	Year         = {2004},
  url          = {http://research.microsoft.com/en-us/um/people/nick/correctnessfull.pdf}
}

@inproceedings{AmtoftB04,
  author       = {Torben Amtoft and
               Anindya Banerjee},
  title        = {Information Flow Analysis in Logical Form},
  booktitle    = sas04,
  pages        = {100--115},
  publisher    = springer,
  series       = lncs,
  volume       = {3148},
  year         = {2004},
  url          = {http://software.imdea.org/~ab/Publications/ifalftr.pdf}
}

@inproceedings{BartheGZ09,
	Author       = {Barthe, Gilles and
                  Gr{\'e}goire, Benjamin and
                  Zanella{-}B{\'e}guelin, Santiago},
	Booktitle    = popl09,
	Pages        = {90--101},
	Title        = {Formal Certification of Code-Based Cryptographic Proofs},
	Year         = {2009},
  url          = {http://research.microsoft.com/pubs/185309/Zanella.2009.POPL.pdf}
}

@inproceedings{BartheDGKZ13,
  author       = {Barthe, Gilles and
                  Danezis, George and
                  Gr{\'e}goire, Benjamin and
                  Kunz, C{\'e}sar and
                  Zanella{-}B{\'e}guelin Santiago},
  title        = {Verified Computational Differential Privacy with Applications to Smart Metering},
  booktitle    = csf13,
  year         = {2013},
  pages        = {287--301},
  url          = {http://www0.cs.ucl.ac.uk/staff/G.Danezis/papers/easypriv.pdf}
}




@inproceedings{DBLP:journals/corr/BaiTG14,
  author       = {Wei Bai and
               Emmanuel M Tadjouddine and
               Yu Guo},
  title        = {Enabling Automatic Certification of Online Auctions},
  booktitle    = fesca14,
  series       = {EPTCS},
  volume       = {147},
  year         = {2014},
  pages        = {123--132},
  url          = {http://dx.doi.org/10.4204/EPTCS.147.9},
}


@inproceedings{DBLP:conf/facs2/BaiTPG13,
  author       = {Wei Bai and
               Emmanuel M Tadjouddine and
               Terry R Payne and
               Sheng-Uei Guan},
  title        = {A Proof-Carrying Code Approach to Certificate Auction Mechanisms},
  booktitle    = {FACS},
  year         = {2013},
  pages        = {23--40},
  url          = {http://dx.doi.org/10.1007/978--3-319--07602--7_4},
  publisher    = springer,
  series       = lncs,
  volume       = {8348},
 }


@inproceedings{DBLP:conf/ceemas/TadjouddineG07,
  author       = {Emmanuel M Tadjouddine and
               Frank Guerin},
  title        = {Verifying Dominant Strategy Equilibria in Auctions},
  booktitle    = ceemas07,
  year         = {2007},
  pages        = {288--297},
  url          = {http://dx.doi.org/10.1007/978--3-540--75254--7_29},
  publisher    = springer,
  series       = lncs,
  volume       = {4696},
}

@article{DBLP:journals/ipl/Vestergaard06,
  author       = {Ren{\'e} Vestergaard},
  title        = {A constructive approach to sequential Nash equilibria},
  journal      = {Inf. Process. Lett.},
  volume       = {97},
  number       = {2},
  year         = {2006},
  pages        = {46--51},
  url          = {http://dx.doi.org/10.1016/j.ipl.2005.09.010},
  bibsource    = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{Roux:2009,
 author        = {Le Roux, St{\'e}phane},
 title         = {Acyclic Preferences and Existence of Sequential Nash
                  Equilibria: {A} Formal and Constructive Equivalence},
 booktitle     = tphol09,
 year          = {2009}
}


@techreport{BUCS-TR-2008-026,
author         = {Andrei Lapets and Alex Levin and David Parkes},
title          = {{A Typed Truthful Language for One-dimensional Truthful Mechanism Design}},
number         = {BUCS-TR-2008--026},
year           = {2008},
institution    = {Boston University},
url            = {http://cs-people.bu.edu/lapets/resource/typed-ec-mech.pdf}
}

@misc{Fang14,
author         = {Ye Fang and Swarat Chaudhuri and  Moshe Vardi},
title          = {{Computer-aided mechanism design}},
howpublished   = {Poster at POPL'14},
year           = {2014}
}


@inproceedings{CasinghinoSW14,
  author       = {Chris Casinghino and Vilhelm Sj\"{o}berg and Stephanie Weirich},
  title        = {Combining Proofs and Programs in a Dependently Typed Langauge},
  booktitle    = popl14,
  year         = {2014},
  url          = {http://www.seas.upenn.edu/~ccasin/papers/combining-TR.pdf}
}

@inproceedings{DBLP:conf/mkm/0002CKMRWW13,
  author       = {Christoph Lange and
                  Marco B Caminati and
                  Manfred Kerber and
                  Till Mossakowski and
                  Colin Rowat and
                  Makarius Wenzel and
                  Wolfgang Windsteiger},
  title        = {A Qualitative Comparison of the Suitability of Four Theorem
               Provers for Basic Auction Theory},
  booktitle    = {MKM/Calculemus/DML},
  publisher    = springer,
  series       = lncs,
  volume       = {7961},
  year         = {2013},
  pages        = {200--215},
  url          = {http://dx.doi.org/10.1007/978--3-642--39320--4_13}
}

@article{DBLP:journals/cacm/ChaudhuriGL12,
  author       = {Swarat Chaudhuri and
                  Sumit Gulwani and
                  Roberto Lublinerman},
  title        = {Continuity and robustness of programs},
  journal      = cacm,
  volume       = {55},
  number       = {8},
  year         = {2012},
  pages        = {107--115},
  url          = {http://dl.acm.org/citation.cfm?id=2240262}
 }

@article{BartheDR04,
  title        = {Secure information flow by self-composition},
  author       = {Barthe, Gilles and
                  D'Argenio, Pedro R. and
                  Rezk, Tamara},
  journal      = mscs,
  volume       = {21},
  number       = {06},
  pages        = {1207--1252},
  year         = {2011},
  publisher    = cup,
  url          = {http://www-sop.inria.fr/lemme/Tamara.Rezk/publication/Barthe-DArgenio-Rezk-Journal.pdf}
}

@inproceedings{ZaksP08,
  author       = {Anna Zaks and Amir Pnueli},
  title        = {{CoVaC}: Compiler Validation by Program Analysis of the Cross-Product},
  booktitle    = fm08,
  pages        = {35--51},
  publisher    = springer,
  series       = lncs,
  volume       = {5014},
  year         = {2008},
  url          = {http://llvm.org/pubs/2008-05-CoVaC.pdf}
}


@inproceedings{TerauchiA05,
	Author       = {Terauchi, Tachio and Aiken, Alex},
	Booktitle    = sas05,
	Pages        = {352--367},
	Publisher    = springer,
	Series       = lncs,
	Title        = {Secure Information Flow as a Safety Problem},
	Volume       = {3672},
	Year         = {2005},
  url          = {http://theory.stanford.edu/~aiken/publications/papers/sas05b.pdf}
}


@inproceedings{BartheCK11,
  author       = {Gilles Barthe and
               Juan Manuel Crespo and
               C{\'e}sar Kunz},
  title        = {Relational Verification Using Product Programs},
  booktitle    = fm11,
  year         = {2011},
  pages        = {200--214},
  series       = lncs,
  volume       = 6664,
  publisher    = springer,
  url          = {http://software.imdea.org/~ckunz/rellog/long-rellog.pdf},
}

@inproceedings{BartheCK13,
  author       = {Gilles Barthe and
                  Juan Manuel Crespo and
                  C{\'e}sar Kunz},
  title        = {Beyond 2-Safety: {Asymmetric} Product Programs for Relational
               Program Verification},
  booktitle    = lfcompsci13,
  year         = {2013},
  pages        = {29--43},
  series       = lncs,
  volume       = 7734,
  publisher    = springer,
  url          = {http://dx.doi.org/10.1007/978--3-642--35722--0_3},
  bibsource    = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:conf/esop/KnowlesF07,
  author       = {Kenneth Knowles and Cormac Flanagan},
  title        = {Type Reconstruction for General Refinement Types},
  booktitle    = esop07,
  year         = {2007},
  pages        = {505--519},
  url          = {http://users.soe.ucsc.edu/~cormac/papers/esop07.pdf}
}

@inproceedings{DBLP:conf/esop/WadlerF09,
  author       = {Philip Wadler and Robert Bruce Findler},
  title        = {Well-Typed Programs Can't Be Blamed},
  booktitle    = esop09,
  year         = {2009},
  pages        = {1--16},
  url          = {http://homepages.inf.ed.ac.uk/wadler/papers/blame/blame.pdf}
}

@inproceedings{DBLP:conf/popl/GreenbergPW10,
  author       = {Michael Greenberg and Benjamin C. Pierce and Stephanie Weirich},
  title        = {Contracts made manifest},
  booktitle    = popl10,
  year         = {2010},
  pages        = {353--364},
  url          = {http://www.cis.upenn.edu/~bcpierce/papers/contracts-popl.pdf}
}

@inproceedings{DBLP:conf/sfp/GronskiF07,
  author       = {Jessica Gronski and Cormac Flanagan},
  title        = {Unifying Hybrid Types and Contracts},
  booktitle    = tfp07,
  year         = {2007},
  pages        = {54--70},
  url          = {https://sage.soe.ucsc.edu/tfp07-gronski-flanagan.pdf}
}

@inproceedings{OngR11,
  title        = {Verifying higher-order functional programs with pattern-matching algebraic data types},
  author       = {Ong, C-H Luke and Ramsay, Steven James},
  booktitle    = popl11,
  pages        = {587--598},
  year         = {2011},
  url          = {https://www.cs.ox.ac.uk/files/3721/main.pdf}
}

@misc{Pierce:2012,
  author       = {Benjamin C. Pierce},
  title        = {Differential Privacy in the Programming Languages Community},
  year         = {2012},
  howpublished = {Invited tutorial at DIMACS Workshop on Recent Work on
               Differential Privacy across Computer Science}
}

@inproceedings{FindlerF02,
  author       = {Robert Bruce Findler and Matthias Felleisen},
  title        = {Contracts for higher-order functions},
  booktitle    = icfp02,
  year         = {2002},
  pages        = {48--59},
  url          = 
  {http://www.eecs.northwestern.edu/~robby/pubs/papers/ho-contracts-techreport.pdf}
}

@INPROCEEDINGS{Augustsson98,
    author     = {Lennart Augustsson},
    title      = {Cayenne -- a Language With Dependent Types},
    booktitle  = icfp98,
    year       = {1998},
    pages      = {239--250},
    url        = {http://link.springer.com/chapter/10.1007%2F10704973_6}
}


@article{Brady13,
  author       = {Edwin Brady},
  title        = {Idris, a general-purpose dependently typed programming language:
               Design and implementation},
  journal      = jfp,
  volume       = {23},
  number       = {5},
  year         = {2013},
  pages        = {552--593},
  url          = {http://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf}
}

@incollection{epigram,
  title       = {Epigram: Practical programming with dependent types},
  author      = {{M}c{B}ride, Conor},
  booktitle   = {Advanced Functional Programming},
  pages       = {130--170},
  year        = {2005},
  publisher   = springer,
  url         = {http://cs.ru.nl/~freek/courses/tt-2010/tvftl/epigram-notes.pdf}
}
@inproceedings{Vytiniotis+13,
 author       = {Vytiniotis, Dimitrios and Peyton Jones, Simon and Claessen, Koen and Ros{\'e}n, Dan},
 title        = {HALO: Haskell to Logic Through Denotational Semantics},
 booktitle    = popl13,
 year         = {2013},
 url          = {http://research.microsoft.com/en-us/people/dimitris/hcc-popl.pdf}
}

@INPROCEEDINGS{Flanagan06,
    author    = {Jessica Gronski and Kenneth Knowles and Aaron Tomb and Stephen N Freund and Cormac Flanagan},
    title     = {Sage: Hybrid checking for flexible specifications},
    booktitle = {Scheme and Functional Programming Workshop},
    year      = {2006},
    pages     = {93--104},
    url       = {http://galois.com/wp-content/uploads/2014/07/pub_AT_SAGEHybridChecking.pdf}
}

@inproceedings{EignerM13,
  author      = {Fabienne Eigner and
               Matteo Maffei},
  title       = {Differential Privacy by Typing in Security Protocols},
  booktitle   = csf13,
  year        = {2013},
  pages       = {272--286},
  url         = {http://sps.cs.uni-saarland.de/publications/dp_proto_long.pdf}
}


@inproceedings{GordonHNR14,
  author      = {Andrew D Gordon and
               Thomas A Henzinger and
               Aditya V Nori and
               Sriram K Rajamani},
  title       = {Probabilistic programming},
  booktitle   = icse14,
  year        = {2014},
  pages       = {167--181},
  url         = {http://research.microsoft.com/pubs/208585/fose-icse2014.pdf}
}
@inproceedings{DaviesP00,
  author      = {Rowan Davies and
               Frank Pfenning},
  title       = {Intersection types and computational effects},
  booktitle   = icfp00,
  year        = {2000},
  pages       = {198--208},
  url         = {http://www.cs.cmu.edu/~fp/papers/icfp00.pdf}
}

@inproceedings{XiP99,
  author      = {Hongwei Xi and
               Frank Pfenning},
  title       = {Dependent Types in Practical Programming},
  booktitle   = popl99,
  year        = {1999},
  pages       = {214--227},
  url         = {http://www.cs.cmu.edu/~fp/papers/popl99.pdf}
}

@inproceedings{DMNS06,
  author    = {Cynthia Dwork and
               Frank {McSherry} and
               Kobbi Nissim and
               Adam D. Smith},
  title     = {Calibrating Noise to Sensitivity in Private Data Analysis},
  booktitle = tcc06,
  volume    = 3876,
  series    = lncs,
  pages     = {265--284},
  year      = {2006},
  url       = {http://dx.doi.org/10.1007/11681878_14},
  doi       = {10.1007/11681878_14},
  publisher = springer
}

@inproceedings{Tschantz201161,
  title       = {Formal Verification of Differential Privacy for Interactive Systems},
  author      = {Tschantz, Michael Carl and
                 Kaynar, Dilsun and
                 Datta, Anupam},
  booktitle   = mfps11,
  series      = entcs,
  volume      = 276,
  pages       = {61--79},
  year        = 2011,
  url         = {http://arxiv.org/pdf/1101.2819v1},
  publisher   = elsevier
}

@article{GHKSW06,
  title       = {Competitive auctions},
  author      = {Goldberg, Andrew V and Hartline, Jason D and Karlin, Anna R and
    Saks, Michael and Wright, Andrew},
  journal     = geb,
  volume      = {55},
  number      = {2},
  year        = {2006},
  pages       = {242--269},
  url         = {http://www.ime.usp.br/~yw/papers/games/goldberg2008-competitive-auctions.pdf},
  publisher   = {Elsevier}
}

@article{mu2008truthful,
  title       = {Truthful approximation mechanisms for restricted combinatorial auctions},
  author      = {{Mu'Alem}, Ahuva and Nisan, Noam},
  journal     = geb,
  volume      = {64},
  number      = {2},
  pages       = {612--631},
  year        = {2008},
  url         = {http://authors.library.caltech.edu/13158/1/MUAgeb08preprint.pdf},
  publisher   = {Elsevier}
}

@inproceedings{milgrom2014deferred,
  title       = {Deferred-acceptance auctions and radio spectrum reallocation},
  author      = {Milgrom, Paul and Segal, Ilya},
  booktitle   = ec14,
  pages       = {185--186},
  year        = {2014},
  url         = {http://web.stanford.edu/~isegal/heuristic.pdf}
}

@article{CKRW14,
  author      = {Rachel Cummings and
               Michael Kearns and
               Aaron Roth and
               Zhiwei Steven Wu},
  title       = {Privacy and Truthful Equilibrium Selection for Aggregative Games},
  journal     = {CoRR},
  year        = {2014},
  volume      = {abs/1407.7740},
  url         = {http://arxiv.org/abs/1407.7740},
  timestamp   = {Sun, 26 Oct 2014 15:36:31 +0100},
  biburl      = {http://dblp.uni-trier.de/rec/bib/journals/corr/CummingsKRW14},
  bibsource   = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{HK12,
  title       = {The exponential mechanism for social welfare: Private, truthful, and nearly optimal},
  author      = {Huang, Zhiyi and Kannan, Sampath},
  booktitle   = focs12,
  pages       = {140--149},
  year        = {2012},
  url         = {http://arxiv.org/abs/1204.1255}
}

@inproceedings{zinkevich,
  author      = {Martin Zinkevich},
  title       = {Online Convex Programming and Generalized Infinitesimal Gradient Ascent},
  booktitle   = icml03,
  year        = {2003},
  pages       = {928--936},
  url         = {http://www.aaai.org/Library/ICML/2003/icml03-120.php},
  timestamp   = {Thu, 16 Oct 2014 21:45:09 +0200},
  biburl      = {http://dblp.uni-trier.de/rec/bib/conf/icml/Zinkevich03},
  bibsource   = {dblp computer science bibliography, http://dblp.org}
}

@article{JKT11,
  title       = {Differentially private online learning},
  author      = {Jain, Prateek and Kothari, Pravesh and Thakurta, Abhradeep Guha},
  journal     = {arXiv preprint arXiv:1109.0105},
  year        = {2011},
  url         = {http://arxiv.org/abs/1109.0105}
}

@inproceedings{JT14,
  title       = {({N}ear) Dimension Independent Risk Bounds for Differentially Private Learning},
  author      = {Jain, Prateek and Thakurta, Abhradeep Guha},
  booktitle   = icml14,
  pages       = {476--484},
  year        = {2014},
  url         = {http://jmlr.org/proceedings/papers/v32/jain14.pdf}
}

@inproceedings{BST14,
  title       = {Differentially Private Empirical Risk Minimization: Efficient
    Algorithms and Tight Error Bounds},
  author      = {Bassily, Raef and Smith, Adam and Thakurta, Abhradeep Guha},
  booktitle   = focs14,
  year        = {2014},
  url         = {http://arxiv.org/abs/1405.7085}
}

@article{dualdecomp,
  title       = {Distributed optimization and statistical learning via the alternating
    direction method of multipliers},
  author      = {Boyd, Stephen and Parikh, Neal and Chu, Eric and Peleato, Borja and
    Eckstein, Jonathan},
  journal     = {Foundations and Trends{\textregistered} in Machine Learning},
  volume      = {3},
  number      = {1},
  pages       = {1--122},
  year        = {2011},
  publisher   = {Now Publishers Inc.},
  url         = {https://web.stanford.edu/~boyd/papers/pdf/admm_distr_stats.pdf}
}

@inproceedings{NST12,
  title       = {Approximately optimal mechanism design via differential privacy},
  author      = {Nissim, Kobbi and Smorodinsky, Rann and Tennenholtz, Moshe},
  booktitle   = itcs12,
  pages       = {203--213},
  year        = {2012},
  url         = {http://arxiv.org/abs/1004.2888}
}

@inproceedings{CCKMV13,
  title       = {Truthful mechanisms for agents that value privacy},
  author      = {Chen, Yiling and Chong, Stephen and Kash, Ian A and Moran, Tal and Vadhan, Salil},
  booktitle   = ec13,
  pages       = {215--232},
  year        = {2013},
  url         = {http://arxiv.org/abs/1111.5472}
}

@inproceedings{Xia13,
  title       = {Is privacy compatible with truthfulness?},
  author      = {Xiao, David},
  booktitle   = itcs13,
  pages       = {67--86},
  year        = {2013},
  url         = {https://eprint.iacr.org/2011/005}
}

@inproceedings{IOh01,
  title       = {{BI} as an assertion language for mutable data structures},
  author      = {Ishtiaq, Samin S and O'Hearn, Peter W},
  booktitle   = popl01,
  year        = 2001,
  url         = {http://dl.acm.org/citation.cfm?id=375719},
  pages       = {14--26}
}

@inproceedings{OhRY01,
  title       = {Local reasoning about programs that alter data structures},
  author      = {O'Hearn, Peter W. and Reynolds, John C. and Yang, Hongseok},
  booktitle   = csl01,
  year        = 2001,
  series      = lncs,
  volume      = 2142,
  publisher   = springer,
  url         = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.29.1331&rep=rep1&type=pdf},
  pages       = {1--19}
}

@inproceedings{DOhY06,
  title       = {A local shape analysis based on separation logic},
  author      = {Distefano, Dino and O'Hearn, Peter W and Yang, Hongseok},
  booktitle   = tacas06,
  year        = 2006,
  url         = {http://dl.acm.org/citation.cfm?id=2182039},
  pages       = {287--302}
}

@inproceedings{BCCC07,
  title       = {Shape analysis for composite data structures},
  author      = {Berdine, Josh and Calcagno, Cristiano and Cook, Byron and
    Distefano, Dino and O'Hearn, Peter W and Wies, Thomas and Yang,
    Hongseok},
  booktitle   = cav07,
  pages       = {178--192},
  url         = {http://research.microsoft.com/pubs/73868/safcds.pdf},
  year        = {2007}
}

@article{Reynolds01,
  title       = {Intuitionistic reasoning about shared mutable data structure},
  author      = {Reynolds, John C.},
  journal     = {Millennial perspectives in computer science},
  volume      = {2},
  number      = {1},
  year        = 2001,
  url         = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.11.5999&rep=rep1&type=pdf},
  pages       = {303--321},
  publisher   = {Palgrave},
  series      = {Cornerstones of Computing},
}

@inproceedings{Reynolds02,
  title       = {Separation logic: {A} logic for shared mutable data structures},
  author      = {Reynolds, John C.},
  booktitle   = lics02,
  year        = 2002,
  pages       = {55--74}
}

@article{Burstall72,
  title       = {Some techniques for proving correctness of programs which alter data structures},
  author      = {Rodnew M. Burstall},
  journal     = {Machine Intelligence},
  volume      = {7},
  number      = {3},
  year        = 1972,
  pages       = {23--50}
}

@inproceedings{smallfoot,
  title       = {Smallfoot: Modular automatic assertion checking with separation logic},
  author      = {Berdine, Josh and Calcagno, Cristiano and O'Hearn, Peter W},
  booktitle   = fmco06,
  pages       = {115--137},
  url         = {http://research.microsoft.com/pubs/67598/smallfoot.pdf},
  year        = {2006}
}

@incollection{VP07,
  title       = {A marriage of rely/guarantee and separation logic},
  author      = {Vafeiadis, Viktor and Parkinson, Matthew},
  booktitle   = concur07,
  pages       = {256--271},
  url         = {http://www.cl.cam.ac.uk/~mjp41/RGSep.pdf},
  year        = 2007
}

@inproceedings{NDQC07,
  title       = {Automated verification of shape and size properties via separation logic},
  author      = {Nguyen, Huu Hai and David, Cristina and Qin, Shengchao and Chin, Wei-Ngan},
  booktitle   = vmcai07,
  pages       = {251--266},
  url         = {http://link.springer.com/chapter/10.1007%2F978-3-540-69738-1_18},
  year        = {2007}
}

@inproceedings{BCOh04,
  title       = {A decidable fragment of separation logic},
  author      = {Berdine, Josh and Calcagno, Cristiano and O'Hearn, Peter W},
  booktitle   = fsttcs04,
  pages       = {97--109},
  url         = {http://research.microsoft.com/pubs/73583/unroll_collapse.pdf},
  year        = 2004
}

@incollection{HAN08,
  title       = {Oracle semantics for concurrent separation logic},
  author      = {Hobor, Aquinas and Appel, Andrew W and Nardelli, Francesco Zappa},
  booktitle   = {Programming Languages and Systems (with ESOP)},
  pages       = {353--367},
  url         = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.116.4226&rep=rep1&type=pdf},
  year        = {2008}
}

@inproceedings{Krebbers14,
  title       = {An operational and axiomatic semantics for non-determinism and sequence points in {C}},
  author      = {Krebbers, Robbert},
  booktitle   = popl14,
  pages       = {101--112},
  url         = {http://robbertkrebbers.nl/research/articles/expressions.pdf},
  year        = {2014}
}

@article{OhP99,
  title       = {The logic of bunched implications},
  author      = {O'Hearn, Peter W and Pym, David J},
  journal     = bsl,
  pages       = {215--244},
  url         = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.27.4742&rep=rep1&type=pdf},
  year        = {1999}
}

@article{POhY04,
  title       = {Possible worlds and resources: The semantics of {BI}},
  author      = {Pym, David J and O'Hearn, Peter W and Yang, Hongseok},
  journal     = tcs,
  volume      = {315},
  number      = {1},
  pages       = {257--305},
  year        = {2004},
  url         = {http://www.sciencedirect.com/science/article/pii/S0304397503006248},
  publisher   = {Elsevier}
}

@inproceedings{BCOh05,
  title       = {Symbolic execution with separation logic},
  author      = {Berdine, Josh and Calcagno, Cristiano and O'Hearn, Peter W},
  booktitle   = aplas05,
  url         = {http://research.microsoft.com/pubs/64175/execution.pdf},
  year        = {2005}
}

@inproceedings{Cousout77,
  title       = {Abstract interpretation: {A} unified lattice model for static
                 analysis of programs by construction or approximation of
                 fixpoints},
  author      = {Cousot, Patrick and Cousot, Radhia},
  booktitle   = popl77,
  pages       = {238--252},
  url         = {http://www.di.ens.fr/~cousot/publications.www/CousotCousot-POPL-77-ACM-p238--252-1977.pdf},
  year        = {1977}
}

@article{Cousout96,
  title       = {Abstract interpretation},
  author      = {Cousot, Patrick},
  journal     = {{ACM} Computing Surveys},
  volume      = {28},
  number      = {2},
  pages       = {324--328},
  year        = {1996},
  url         = {http://dl.acm.org/citation.cfm?id=234740},
}

@inproceedings{dwork2010pan,
  title       = {Pan-Private Streaming Algorithms.},
  author      = {Dwork, Cynthia and
               Naor, Moni and
               Pitassi, Toniann and
               Rothblum, Guy N and
               Yekhanin, Sergey},
  booktitle   = itcs10,
  pages       = {66--80},
  url         = {http://www.cs.toronto.edu/~toni/Papers/panprivacy.pdf},
  year        = {2010}
}

@inproceedings{recommender,
  title       = {Differentially private recommender systems: building privacy into the net},
  author      = {{McSherry}, Frank and Mironov, Ilya},
  booktitle   = kdd09,
  pages       = {627--636},
  year        = {2009},
  url         = {http://research.microsoft.com/pubs/80511/netflixprivacy.pdf}
}

@book{cvxbook,
 author       = {Boyd, Stephen and Vandenberghe, Lieven},
 title        = {Convex Optimization},
 year         = {2004},
 isbn         = {0521833787},
 publisher    = cup,
}

@book{concentration-book,
  title       = {Concentration of measure for the analysis of randomized algorithms},
  author      = {Dubhashi, Devdatt P and Panconesi, Alessandro},
  year        = {2009},
  publisher   = cup
}

@article{LovaszLocal,
  title       = {Problems and results on 3-chromatic hypergraphs and some related
    questions},
  author      = {Erdos, Paul and Lov{\'a}sz, L{\'a}szl{\'o}},
  journal     = {Infinite and finite sets},
  volume      = {10},
  pages       = {609--627},
  year        = {1975}
}

@article{erdosPM,
  title       = {Graph theory and probability},
  author      = {Paul Erd{\H{o}}s},
  journal     = {Canadian Journal of Mathematics},
  volume      = {11},
  pages       = {34--38},
  year        = {1959}
}

@inproceedings{DBLP:conf/pldi/SampsonPMMGC14,
  author      = {Adrian Sampson and
               Pavel Panchekha and
               Todd Mytkowicz and
               Kathryn S McKinley and
               Dan Grossman and
               Luis Ceze},
  title       = {Expressing and verifying probabilistic assertions},
  booktitle   = pldi14,
  pages       = {112--122},
  year        = {2014},
  url         = {http://doi.acm.org/10.1145/2594291.2594294},
} 

@article{alea,
  title       = {Proofs of randomized algorithms in {C}oq},
  author      = {Audebaud, Philippe and Paulin-Mohring, Christine},
  journal     = {Science of Computer Programming},
  volume      = {74},
  number      = {8},
  pages       = {568--589},
  year        = {2009},
  publisher   = elsevier
}

@inproceedings{DBLP:conf/pldi/SampsonPMMGC14,
  author      = {Adrian Sampson and
               Pavel Panchekha and
               Todd Mytkowicz and
               Kathryn S McKinley and
               Dan Grossman and
               Luis Ceze},
  title       = {Expressing and verifying probabilistic assertions},
  booktitle   = pldi14,
  pages       = {14},
  year        = {2014},
  url         = {http://doi.acm.org/10.1145/2594291.2594294},
} 
@inproceedings{DBLP:conf/pldi/CarbinKMR12,
  author      = {Michael Carbin and
               Deokhwan Kim and
               Sasa Misailovic and
               Martin C Rinard},
  title       = {Proving acceptability properties of relaxed nondeterministic approximate
               programs},
  booktitle   = pldi12,
  pages       = {169--180},
  year        = {2012},
  url         = {http://doi.acm.org/10.1145/2254064.2254086},
}

@InProceedings{Necula97,
  author      = "G. C. Necula",
  title       = "Proof-carrying code",
  booktitle   = popl97,
  year        = "1997",
  pages       = "106--119",
}

@inproceedings{BartheGHZ11,
  author      = {Barthe, Gilles and
                 Gr{\'e}goire, Benjamin  and
                 Heraud, Sylvain  and
                 Zanella{-}B{\'e}guelin, Santiago},
  title       = {Computer-Aided Security Proofs for the Working Cryptographer},
	Booktitle   = crypto11,
  year        = {2011},
	Pages       = {71--90},
  publisher   = springer,
  series      = lncs,
  volume      = {6841},
  url         = {http://software.imdea.org/~szanella/Zanella.2011.CRYPTO.pdf},
  bibsource   = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{flanagan2001,
  title       = {Avoiding exponential explosion: Generating compact 
verification conditions},
  author      = {Flanagan, Cormac and Saxe, James B},
  booktitle   = popl01,
  pages       = {193--205},
  year        = {2001},
}

@inproceedings{BartheDGKSS13,
  author    = {Gilles Barthe and
               Fran{\c{c}}ois Dupressoir and
               Benjamin Gr{\'{e}}goire and
               C{\'{e}}sar Kunz and
               Benedikt Schmidt and
               Pierre{-}Yves Strub},
  title     = {EasyCrypt: {A} Tutorial},
  booktitle = {Foundations of Security Analysis and Design ({FOSAD})},
  series    = lncs,
  volume    = {8604},
  pages     = {146--166},
  publisher = springer,
  year      = {2013},
  note      = {Tutorial Lectures},
}

@article{hoare1969axiomatic,
  title={An axiomatic basis for computer programming},
  author={Hoare, Charles A. R.},
  journal=cacm,
  volume={12},
  number={10},
  pages={576--580},
  year={1969},
}

@incollection{Floyd67,
    author     = {Floyd, Robert W.},
    booktitle  = {Symposium on Applied Mathematics},
    publisher  = {American Mathematical Society},
    title      = {{Assigning meanings to programs}},
    year       = {1967}
}


@article{Cook:1978,
	Author       = {Cook, S.},
	Journal      = siamjc,
	Number       = {1},
	Pages        = {70--90},
	Title        = {Soundness and Completeness of an Axiom System for Program Verification},
	Volume       = {7},
	Year         = {1978}
}

@inproceedings{Clarkson:2008,
  title={Hyperproperties},
  author={Clarkson, Michael R and Schneider, Fred B},
  journal={Journal of Computer Security},
  volume={18},
  number={6},
  pages={1157--1210},
  year={2010},
  publisher={IOS Press}
}

@InProceedings{Turing:1949,
  author       = "Alan M. Turing",
  title        = "Checking a Large Routine",
  pages        = "67--69",
  year         = "1949",
  URL          = "http://www.turingarchive.org/browse.php/B/8",
 booktitle     = "{Report on a Conference on High Speed Automatic
                 Computation, June 1949}",
}


@inproceedings{HM07,
  title        = {The communication complexity of uncoupled nash equilibrium procedures},
  author       = {Hart, Sergiu and Mansour, Yishay},
  booktitle    = stoc07,
  pages        = {345--353},
  year         = {2007},
}

@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},
}

@inproceedings{CS02,
  title        = {Complexity of mechanism design},
  author       = {Conitzer, Vincent and Sandholm, Tuomas},
  booktitle    = uai02,
  pages        = {103--110},
  year         = {2002},
  organization = {Morgan Kaufmann Publishers Inc.}
}

@inproceedings{San03,
  title        = {Automated mechanism design: {A} new application area for search algorithms},
  author       = {Sandholm, Tuomas},
  booktitle    = cp03,
  pages        = {19--36},
  year         = {2003},
  organization = springer
}

@inproceedings{BP14,
  title        = {Verifiably Truthful Mechanisms},
  author       = {Br{\^a}nzei, Simina and Procaccia, Ariel D},
  booktitle    = itcs14,
  year         = {2014}
}

@phdthesis{Con06,
  title        = {Computational aspects of preference aggregation},
  author       = {Conitzer, Vincent},
  year         = {2006},
  school       = {IBM}
}

@inproceedings{HKM11,
  title        = {Bayesian incentive compatibility via matchings},
  author       = {Hartline, Jason D and Kleinberg, Robert and Malekian, Azarakhsh},
  booktitle    = soda11,
  pages        = {734--747},
  year         = {2011},
}

@inproceedings{BH11,
  title        = {Bayesian incentive compatibility via fractional assignments},
  author       = {Bei, Xiaohui and Huang, Zhiyi},
  booktitle    = soda11,
  pages        = {720--733},
  year         = {2011},
}

@book{Rou05,
  title        = {Selfish routing and the price of anarchy},
  author       = {Roughgarden, Tim},
  volume       = {174},
  year         = {2005},
  publisher    = mitpress
}

@article{Morgan:1996,
  author    = {Carroll Morgan and
               Annabelle McIver and
               Karen Seidel},
  title        = {Probabilistic Predicate Transformers},
  journal      = toplas,
  volume       = {18},
  number       = {3},
  year         = {1996},
  pages     = {325--353}
}

@article{Kozen:1985,
  author       = {Dexter Kozen},
  title        = {A Probabilistic {PDL}},
  journal      = jcss,
  volume       = {30},
  number       = {2},
  year         = {1985}
}

@article{Morgan:1996,
  author       = {C Morgan and
               A Mc{I}ver and
               K Seidel},
  title        = {Probabilistic Predicate Transformers},
  journal      = toplas,
  volume       = {18},
  number       = {3},
  year         = {1996}
}

@article{Kozen:1985,
  author       = {D. Kozen},
  title        = {A Probabilistic {PDL}},
  journal      = jcss,
  volume       = {30},
  number       = {2},
  year         = {1985}
}

@inproceedings{TGV09,
year           = {2009},
booktitle      = {Declarative Agent Languages and Technologies VI},
volume         = {5397},
series         = lncs,
title          = {Abstracting and Verifying Strategy-Proofness for Auction Mechanisms},
publisher      = springer,
author         = {Tadjouddine, Emmanuel M. and Guerin, Frank and Vasconcelos, Wamberto},
pages          = {197--214},
}


@inproceedings{DBLP:conf/ceemas/TadjouddineG07,
  author       = {Emmanuel M Tadjouddine and
               Frank Guerin},
  title        = {Verifying Dominant Strategy Equilibria in Auctions},
  booktitle    = {{CEEMAS 2007}},
  year         = {2007},
  pages        = {288--297},
  publisher    = springer,
  series       = lncs,
  volume       = {4696},
}

@inproceedings{DBLP:journals/corr/BaiTG14,
  author       = {Wei Bai and
               Emmanuel M Tadjouddine and
               Yu Guo},
  title        = {Enabling Automatic Certification of Online Auctions},
  booktitle    = {{FESCA 2014}},
  series       = {EPTCS},
  volume       = {147},
  year         = {2014},
  pages        = {123--132},
  url          = {http://dx.doi.org/10.4204/EPTCS.147.9},
}

@incollection{DBLP:conf/mkm/0002CKMRWW13,
  author       = {Christoph Lange and
               Marco B Caminati and
               Manfred Kerber and
               Till Mossakowski and
               Colin Rowat and
               Makarius Wenzel and
               Wolfgang Windsteiger},
  title        = {A Qualitative Comparison of the Suitability of Four Theorem
               Provers for Basic Auction Theory},
  booktitle    = {Intelligent Computer Mathematics},
  publisher    = springer,
  series       = lncs,
  volume       = {7961},
  year         = {2013},
  pages        = {200--215},
  url          = {http://dx.doi.org/10.1007/978--3-642--39320--4_13},
  publisher    = springer
}

@article{DBLP:journals/ipl/Vestergaard06,
  author       = {Ren{\'e} Vestergaard},
  title        = {A constructive approach to sequential Nash equilibria},
  journal      = {Inf. Process. Lett.},
  volume       = {97},
  number       = {2},
  year         = {2006},
  pages        = {46--51},
  url          = {http://dx.doi.org/10.1016/j.ipl.2005.09.010},
  bibsource    = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/aaai/WooldridgeADH07,
  author       = {Wooldridge, Michael and
               {Agotnes}, Thaoms and
               Dunne, Paul E. and
               van der Hoek, Wiebe},
  title        = {Logic for Automated Mechanism Design---{A} Progress Report},
  booktitle    = aaai07,
  pages        = {9--17},
  year         = {2007},
}

@Article{Alur:2002:ATT,
  author       = "Rajeev Alur and Thomas A. Henzinger and Orna Kupferman",
  title        = "Alternating-time temporal logic",
  journal      = jacm,
  volume       = "49",
  number       = "5",
  pages        = "672--713",
  year         = "2002",
  journal-url  = "http://portal.acm.org/browse_dl.cfm?idx = J401",
}

@inproceedings{Gonthier13,
  author       = {Georges Gonthier and
               Andrea Asperti and
               Jeremy Avigad and
               Yves Bertot and
               Cyril Cohen and
               Fran{\c{c}}ois Garillot and
               St{\'{e}}phane Le Roux and
               Assia Mahboubi and
               Russell O'{C}onnor and
               Sidi Ould Biha and
               Ioana Pasca and
               Laurence Rideau and
               Alexey Solovyev and
               Enrico Tassi and
               Laurent Th{\'{e}}ry},
  title        = {A Machine-Checked Proof of the Odd Order Theorem},
  booktitle    = {Interactive Theorem Proving (ITP)},
  pages        = {163--179},
  year         = {2013},
}

@article{clarke71,
  title        = {Multipart pricing of public goods},
  author       = {Clarke, Edward H},
  journal      = {Public choice},
  volume       = {11},
  number       = {1},
  pages        = {17--33},
  year         = {1971},
  publisher    = springer
}

@article{groves73,
  title        = {Incentives in teams},
  author       = {Groves, Theodore},
  journal      = {Econometrica: Journal of the Econometric Society},
  pages        = {617--631},
  year         = {1973}
}

@inproceedings{Bellare:2006,
  author       = {Bellare, Mihir and Rogaway, Phillip},
  booktitle    = eucrypt06,
  pages        = {409--426},
  publisher    = springer,
  series       = lncs,
  title        = {The Security of Triple Encryption and a Framework for
    Code-Based Game-Playing Proofs},
  volume       = {4004},
  year         = {2006},
  url          = {https://www.iacr.org/archive/eurocrypt2006/40040415/40040415.pdf}
}

@misc{Halevi:2005,
  author       = {Halevi, Shai},
  howpublished = {Cryptology ePrint Archive, Report 2005/181},
  title        = {A plausible approach to computer-aided cryptographic proofs},
  year         = {2005},
  url          = {https://eprint.iacr.org/2005/181.pdf}
}


@misc{Shoup:2004,
  author       = {Shoup, Victor},
  howpublished = {Cryptology ePrint Archive, Report 2004/332},
  title        = {Sequences of games: {A} tool for taming complexity in security proofs},
  year         = {2004}
}

@unpublished{Naumann:2009,
  author       = {Naumann, David A},
  title        = {Theory for software verification},
  year         = {2009},
  url          = {http://www.cs.stevens.edu/~naumann/publications/theoryverif.pdf}
}

@incollection{handbook-sat,
  title        = {Satisfiability Modulo Theories},
  author       = {Barrett, Clark and Sebastini, Roberto and Seshia, Sanjit A and
    Tinelli, Cesare},
  booktitle    = {Handbook of satisfiability},
  volume       = {185},
  year         = {2009},
  publisher    = {IOS press},
}

@inproceedings{HPN11,
  title        = {Differential Privacy Under Fire},
  author       = {Haeberlen, Andreas and
          Pierce, Benjamin C. and
          Narayan, Arjun},
  booktitle    = {USENIX Security Symposium},
  year         = {2011}
}

@article{Girard87,
  title        = {{Linear logic}},
  author       = {Girard, J.Y.},
  journal      = tcs,
  volume       = {50},
  number       = {1},
  pages        = {1--102},
  year         = {1987},
  publisher    = {Elsevier}
}

@incollection{Walker-atapl,
  author       = {David Walker},
  title        = {Substructural Type Systems},
  booktitle    = {Advanced Topics in Types and Programming Languages},
  editor       = {Benjamin C. Pierce},
  publisher    = mitpress,
  year         = {2005},
}

@article{BLL,
  title        = {{Bounded linear logic}},
  author       = {Girard, J.Y. and Scedrov, A. and Scott, P.},
  journal      = tcs,
  volume       = {97},
  number       = {1},
  pages        = {1--66},
  year         = {1992}
}

@inproceedings{WrightBaker93,
  title        = {{Usage Analysis with Natural Reduction Types}},
  author       = {Wright, D.A. and Baker-Finch, C.A.},
  booktitle    = {International Workshop on Static Analysis},
  pages        = {254--266},
  year         = {1993},
  publisher    = springer
}

@InProceedings{DalLagoHofmann09,
  title        = "Bounded Linear Logic, Revisited",
  author       = "Dal Lago, Ugo and Hofmann, Martin",
  booktitle    = tlca,
  publisher    = springer,
  year         = "2009",
  volume       = "5608",
  pages        = "80--94",
  series       = lncs,
}

@InProceedings{XiPfenning99,
  author       = "Hongwei Xi and Frank Pfenning",
  title        = "Dependent Types in Practical Programming",
  pages        = "214--227",
  booktitle    = popl99,
  year         = "1999",
}

@InProceedings{ATS,
  title        = "Combining programming with theorem proving",
  author       = "Chiyan Chen and Hongwei Xi",
  booktitle    = icfp05,
  year         = "2005",
  pages        = "66--77",
  url          = "http://doi.acm.org/10.1145/1086365.1086375",
}

@article{McBrideMcKinna02,
  author       = {Conor Mc{B}ride and James Mc{K}inna},
  title        = {The view from the left},
  journal      = jfp,
  year         = {2004}, 
  pages        = "69--111",
  volume       = 14,
  number       = 1,
}

@inproceedings{weirich-promotion,
  author       = {Yorgey, Brent A and
            Weirich, Stephanie and 
            Cretin, Julien and
            {Peyton Jones}, Simon and 
            Vytiniotis, Dimitrios and
            Magalha\~{e}s, Jos\'{e} Pedro},
  title        = {Giving Haskell A Promotion},
  booktitle    = tldi12,
  year         = 2012,
  url          = {http://www.seas.upenn.edu/~sweirich/papers/tldi12.pdf},
}

@Article{cervesato-llf,
  title        = "A Linear Logical Framework",
  author       = "Iliano Cervesato and Frank Pfenning",
  journal      = ic,
  year         = "2002",
  volume       = "179",
  number       = "1",
  pages        = "19--75",
}

@InProceedings{watkins03types,
  author       = "Keven Watkins and Iliano Cervesato and Frank Pfenning
		 and David Walker",
  title        = "A concurrent logical framework {I}: The propositional
		 fragment",
  booktitle    = types,
  volume       = 3085,
  series       = lncs, 
  publisher    = springer,
  year         = "2003",
}

@InProceedings{DLG11,
author         = {Dal Lago, Ugo and
         Gaboardi, Marco},
title          = "Linear Dependent Types and Relative Completeness",
  booktitle    = lics11,
 pages         = "133--142",
year           = {2011}
}

@InProceedings{KTDG12,
  title        = "Superficially Substructural Types",
  author       = "Krishnaswami, Neelakantan R. and Turon, Aaron and Dreyer, Derek and Garg, Deepak",
  booktitle    = icfp12,
  year         = 2012,
}

@inproceedings{CGL10,
 author        = {Chaudhuri, Swarat and Gulwani, Sumit and Lublinerman, Roberto},
 title         = {Continuity analysis of programs},
 booktitle     = popl10,
 year          = {2010},
 pages         = {57--70},
}

@InProceedings{CGLN11,
  title        = "Proving programs robust",
  author       = "Swarat Chaudhuri and Sumit Gulwani and Roberto
		 Lublinerman and Sara NavidPour",
  booktitle    = esecfse11,
  year         = "2011",
  ISBN         = "978-1-4503-0443-6",
  pages        = "102--112",
  URL          = "http://doi.acm.org/10.1145/2025113.2025131",
}

@INPROCEEDINGS{Lowe-QIF02,
    author     = {Gavin Lowe},
    title      = {Quantifying Information Flow},
    booktitle  = csfw02,
    year       = {2002},
    pages      = {18--31}
}

@inproceedings{McCamantErnst08,
 author        = {McCamant, Stephen and Ernst, Michael D.},
 title         = {Quantitative information flow as network flow capacity},
 booktitle     = pldi08,
 year          = {2008},
 isbn          = {978-1-59593-860-2},
 pages         = {193--205},
 }

@inproceedings{AACP11,
  author       = {Alvim, S., M{\'a}rio and Andres, E., Miguel and Chatzikokolakis, Konstantinos and Palamidessi, Catuscia},
  title        = {{On the relation between Differential Privacy and Quantitative Information Flow}},
  booktitle    = icalp11,
  year         = {2011},
  series       = lncs,
  publisher    = springer,
  volume       = {6756},
  pages        = {60--76},
  url          = {http://hal.inria.fr/inria-00627937/en},
}

@inproceedings{barthekoepf11,
 author        = {Gilles Barthe and Boris K{\"o}pf},
 title         = {{Information-theoretic Bounds for Differentially Private Mechanisms}},
 booktitle     = csf11,
 publisher     = ieee,
 pages         = {191--204},
 year          = {2011}
}

@inproceedings{AgrawalSrikant00,
  title        = {Privacy-preserving data mining},
  author       = {Agrawal, Rakesh and Srikant, Ramakrishnan},
  booktitle    = sigmod00,
  pages        = {439--450},
  year         = {2000},
}

@article{l-diversity,
  title        = {l-diversity: Privacy beyond k-anonymity},
  author       = {Machanavajjhala, Ashwin and Kifer, Daniel and Gehrke, Johannes and
    Venkitasubramaniam, Muthuramakrishnan},
  journal      = {{ACM} Transactions on Knowledge Discovery from Data ({TKDD})},
  volume       = {1},
  number       = {1},
  pages        = {3},
  year         = {2007},
}

@article{ESA04,
  title        = {Privacy preserving mining of association rules},
  author       = {Evfimievski, Alexandre and Srikant, Ramakrishnan and Agrawal,
    Rakesh and Gehrke, Johannes},
  journal      = {Information Systems},
  volume       = {29},
  number       = {4},
  pages        = {343--364},
  year         = {2004},
  publisher    = elsevier
}

@inproceedings{GKSS08,
  title        = {Composition attacks and auxiliary information in data privacy},
  author       = {Ganta, Srivatsava Ranjit and Kasiviswanathan, Shiva Prasad and
    Smith, Adam},
  booktitle    = kdd08,
  pages        = {265--273},
  year         = {2008},
}

@book{Hurwicz60,
  title        = {Optimality and informational efficiency in resource allocation
    processes},
  author       = {Hurwicz, Leonid},
  year         = {1960},
  publisher    = {Stanford University Press}
}

@article{Vickrey61,
  title        = {Counterspeculation, auctions, and competitive sealed tenders},
  author       = {Vickrey, William},
  journal      = {The Journal of Finance},
  volume       = {16},
  number       = {1},
  pages        = {8--37},
  year         = {1961},
}

@article{Hurwicz72,
  title        = {On informationally decentralized systems},
  author       = {Hurwicz, Leonid},
  journal      = {Decision and organization},
  year         = {1972},
  publisher    = {North-Holland Amsterdam}
}

@article{Myerson08,
  title        = {Perspectives on mechanism design in economic theory},
  author       = {Myerson, Roger B},
  journal      = {The American Economic Review},
  pages        = {586--603},
  year         = {2008},
  publisher    = {JSTOR}
}

@incollection{BGBP-bigops08,
  title        = {Canonical big operators},
  author       = {Bertot, Yves and Gonthier, Georges and Biha, Sidi Ould and Pasca,
    Ioana},
  booktitle    = tphol,
  pages        = {86--101},
  year         = {2008},
  publisher    = springer
}

@phdthesis{Ramshaw79,
  title        = {Formalizing the Analysis of Algorithms.},
  author       = {Ramshaw, Lyle Harold},
  year         = {1979},
  school       = {Stanford University},
  note         = {STAN-CS-79-741}
}

@article{HartogVink02,
  title        = {Verifying probabilistic programs using a {H}oare like logic},
  author       = {den Hartog, J I and de Vink, Erik P},
  journal      = {International Journal of Foundations of Computer Science},
  volume       = {13},
  number       = {03},
  pages        = {315--340},
  year         = {2002},
  publisher    = {World Scientific}
}

@article{Chadha07,
  title        = {Reasoning about probabilistic sequential programs},
  author       = {Chadha, Rohit and Cruz-Filipe, Lu{\'\i}s and Mateus, Paulo and
    Sernadas, Am{\'\i}lcar},
  journal      = tcs,
  volume       = {379},
  number       = {1},
  pages        = {142--165},
  year         = {2007},
  publisher    = elsevier
}

@misc{RandZdancewic15,
  author       = {Rand, Robert and Zdancewic, Steve},
  title        = {A Formally Verified Probabilistic {H}oare Logic with Non-Termination},
  year         = 2015
}

inproceedings{Kozen79,
	Author = {Kozen, Dexter},
	Booktitle = focs79,
	Pages = {101--114},
	Title = {Semantics of probabilistic programs},
	Year = {1979}}

@article{Kozen81,
  title        = {Semantics of probabilistic programs},
  author       = {Kozen, Dexter},
  journal      = {Journal of Computer and System Sciences},
  volume       = {22},
  number       = {3},
  pages        = {328--350},
  year         = {1981},
  publisher    = {Elsevier}
}

@article{HSP83,
  title        = {Termination of probabilistic concurrent program},
  author       = {Hart, Sergiu and Sharir, Micha and Pnueli, Amir},
  journal      = toplas,
  volume       = {5},
  number       = {3},
  pages        = {356--380},
  year         = {1983},
}

@inproceedings{Hurd02,
  title        = {A formal approach to probabilistic termination},
  author       = {Hurd, Joe},
  booktitle    = tphol,
  pages        = {230--245},
  year         = {2002},
  publisher    = springer
}

@inproceedings{Chakarov-martingale,
  title        = {Probabilistic program analysis with martingales},
  author       = {Chakarov, Aleksandar and Sankaranarayanan, Sriram},
  booktitle    = cav13,
  pages        = {511--526},
  year         = {2013},
  url          = {https://www.cs.colorado.edu/~srirams/papers/cav2013-martingales.pdf}
}

@inproceedings{FerrerHermanns15,
  title        = {Probabilistic Termination: Soundness, Completeness, and
    Compositionality},
  author       = {Ferrer Fioriti, Luis Mar{\'\i}a and Hermanns, Holger},
  booktitle    = popl15,
  pages        = {489--501},
  year         = {2015},
  url          = {http://www.ae-info.org/attach/User/Hermanns_Holger/Publications/FH-POPL15.pdf},
}

@inproceedings{Kozen06,
  title        = {Coinductive Proof Principles for Stochastic Processes},
  author       = {Kozen, Dexter},
  booktitle    = lics06,
  pages        = {359--366},
  year         = {2006},
  organization = ieee
}

@inproceedings{liquid-haskell,
  title        = {Abstract refinement types},
  author       = {Vazou, Niki and Rondon, Patrick M and Jhala, Ranjit},
  booktitle    = esop13,
  pages        = {209--228},
  year         = {2013},
  publisher    = springer
}

@inproceedings{liquid-ml,
  title        = {Liquid types},
  author       = {Rondon, Patrick M and Kawaguci, Ming and Jhala, Ranjit},
  booktitle    = pldi08,
  volume       = {43},
  number       = {6},
  pages        = {159--169},
  year         = {2008},
}

@book{Thorisson00,
  author       = {Hermann Thorisson},
  title        = {Coupling, Stationarity, and Regeneration},
  publisher    = springer,
  year         = {2000}
}

@book{Lindvall02,
  title        = {Lectures on the coupling method},
  author       = {Lindvall, Torgny},
  year         = {2002},
  publisher    = {Courier Corporation}
}

@techreport{DengD11,
	Author       = {Deng, Yuxin and Du, Wenjie},
	Institution  = {Carnegie Mellon University},
	Month        = {March},
	Number       = {CMU-CS-11-110},
	Title        = {Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation},
	Year         = {2011}, 
  url          = {http://arxiv.org/abs/1103.4577}
}

@article{Yang07,
  author       = {Hongseok Yang},
  title        = {Relational separation logic},
  journal      = tcs,
  volume       = 375,
  number       = {1--3},
  year         = 2007,
  pages        = {308--334},
  url          = {http://www.cs.ox.ac.uk/people/hongseok.yang/paper/data.pdf}
}

@article{mufa1994optimal,
  title        = {Optimal Markovian couplings and applications},
  author       = {Mufa, Chen},
  journal      = {Acta Mathematica Sinica},
  volume       = {10},
  number       = {3},
  pages        = {260--275},
  year         = {1994},
  publisher    = springer
}

@article{mount1974informational,
  title={The informational size of message spaces},
  author={Mount, Kenneth and Reiter, Stanley},
  journal=jet,
  volume={8},
  number={2},
  pages={161--192},
  year={1974},
  url={http://www.kellogg.northwestern.edu/faculty/reiter/papers/22_informationalsize.pdf},
  publisher={Elsevier}
}

@inproceedings{devanur2011prior,
  title={Prior-independent multi-parameter mechanism design},
  author={Devanur, Nikhil and Hartline, Jason and Karlin, Anna and Nguyen, Thach},
  booktitle=wine11,
  pages={122--133},
  year={2011},
  publisher=springer,
  url={http://users.eecs.northwestern.edu/~hartline/papers/auctions-WINE-11.pdf},
}

@inproceedings{CR14,
 author = {Cole, Richard and Roughgarden, Tim},
 title = {The Sample Complexity of Revenue Maximization},
 booktitle = stoc14,
 year = {2014},
 pages = {243--252},
 numpages = {10},
 url={http://arxiv.org/abs/1502.00963},
 keywords = {Myerson's auction, sample complexity},
} 

@inproceedings{blum2005near,
  author = {Blum, Avrim and Hartline, Jason D},
  booktitle = soda05,
  pages = {1156--1163},
  publisher = siam,
  title = {Near-optimal online auctions},
  url={http://users.eecs.northwestern.edu/~hartline/papers/online-auctions-SODA-05.pdf},
  year = 2005
}

@inproceedings{balcan2005mechanism,
  author    = {Balcan, Maria{-}Florina and
               Blum, Avrim and
               Hartline, Jason D and
               Mansour, Yishay},
  title     = {Mechanism Design via Machine Learning},
  booktitle = focs05,
  pages     = {605--614},
  url       = {http://users.eecs.northwestern.edu/~hartline/papers/auctions-FOCS-05.pdf},
  year      = 2005,
}

@INPROCEEDINGS {B+03,
    author    = {Blum, Avrim and Kumar, Vijay and Rudra, Atri and Wu, Felix},
    title     = "Online Learning in Online Auctions",
    booktitle = soda03,
    url       = {http://www.cs.cmu.edu/~avrim/Papers/onlineauction.pdf},
    year      = 2003,
}

@inproceedings{CGMsoda13,
  author = {Cesa-Bianchi, Nicolò and Gentile, Claudio and Mansour, Yishay},
  booktitle = soda13,
  pages = {1190--1204},
  publisher = siam,
  title = {Regret Minimization for Reserve Prices in Second-Price Auctions},
  url  = {http://epubs.siam.org/doi/pdf/10.1137/1.9781611973105.86},
  year = 2013
}


@inproceedings{hartline2009simple,
  author = {Hartline, Jason D and Roughgarden, Tim},
  booktitle = ec09,
  title = {Simple versus optimal mechanisms},
  year = 2009,
  url = {http://www.sigecom.org/exchanges/volume_8/1/hartline.pdf},
}


@Inproceedings {BBDSics11,
author       = {Babaioff, Moshe and Blumrosen, Liad and Dughmi, Shaddin and Singer, Yaron},
booktitle    = itcs11,
publisher    = {Tsinghua University Press},
title        = {Posting Prices with Unknown Distributions},
year         = {2011},
url          = {http://research.microsoft.com/apps/pubs/default.aspx?id=144123},
}


@inproceedings {morgenstern15pseudo,
    author  = {Jamie Morgenstern and Tim Roughgarden},
    title   = {The Pseudo-Dimension of Nearly-Optimal Auctions},
    booktitle = nips15,
    year    = 2015,
    url     = {http://arxiv.org/abs/1506.03684},
}

@inproceedings{RS15,
  author = "Roughgarden, Tim and Schrijvers, Okke",
  title = "Ironing in the Dark",
  booktitle = ec16,
  pages = {1-18},
  year = 2016,
  url = {https://arxiv.org/abs/1511.06918},
}

@inproceedings{rubensteinsubadditive,
 author = {Rubinstein, Aviad and Weinberg, S. Matthew},
 title = {Simple Mechanisms for a Subadditive Buyer and Applications to Revenue Monotonicity},
 booktitle = ec15,
 year = {2015},
 pages = {377--394},
 url = {http://people.csail.mit.edu/smweinberg/ec15subadditive.pdf},
}

@inproceedings{balcan2014learning,
  title={Learning economic parameters from revealed preferences},
  author={Balcan, Maria-Florina and Daniely, Amit and Mehta, Ruta and Urner, Ruth and Vazirani, Vijay V},
  booktitle=wine14,
  pages={338--353},
  year={2014},
  publisher=springer,
  url={http://arxiv.org/abs/1407.7937}
}

@inproceedings{dughmi2014sampling,
year={2014},
booktitle=wine14,
volume={8877},
series=lncs,
title={Sampling and Representation Complexity of Revenue Maximization},
publisher=springer,
author={Dughmi, Shaddin and Han, Li and Nisan, Noam},
pages={277--291},
url={http://arxiv.org/abs/1402.4535},
}


@inproceedings{babaioffadditive,
	Author = {Babaioff, Moshe and Immorlica, Nicole and Lucier, Brendan and
    Weinberg, S. Matthew},
	Booktitle = focs14,
	Title = {A Simple and Approximately Optimal Mechanism for an Additive Buyer},
	Year = {2014},
  url  = {http://arxiv.org/abs/1405.6146}
}

@inproceedings{yao2015soda,
author = {Yao, Andrew Chi-Chih},
title = {An $n$-to-$1$ Bidder Reduction for Multi-item Auctions and its Applications},
booktitle = soda14,
chapter = {8},
year={2015},
pages = {92--109},
url = {http://arxiv.org/abs/1406.3278}
}


@inproceedings{huang2014making,
 author = {Huang, Zhiyi and Mansour, Yishay and Roughgarden, Tim},
 title = {Making the Most of Your Samples},
 booktitle = ec15,
 year = {2015},
 isbn = {978-1-4503-3410-5},
 pages = {45--60},
 keywords = {auction, revenue, sample complexity},
 url = {http://arxiv.org/abs/1407.2479},
} 

@article{dhangwatnotai2014revenue,
  title={Revenue maximization with a single sample},
  author={Dhangwatnotai, Peerapong and Roughgarden, Tim and Yan, Qiqi},
  journal=geb,
  year={2014},
  publisher={Elsevier},
  url={http://theory.stanford.edu/~tim/papers/single.pdf},
}


@inproceedings{chawla2007algorithmic,
 author = {Chawla, Shuchi and Hartline, Jason and Kleinberg, Robert},
 title = {Algorithmic Pricing via Virtual Valuations},
 booktitle = ec07,
 year = {2007},
 pages = {243--251},
 url = {http://arxiv.org/abs/0808.1671},
} 

@article{GS99a,
title = "The {E}nglish Auction with Differentiated Commodities",
journal = jet,
volume = "92",
number = "1",
pages = "66--95",
year = "2000",
issn = "0022-0531",
url = "http://www.sciencedirect.com/science/article/pii/S0022053199925802",
author = "Faruk Gul and Ennio Stacchetti"
}


@Article{OL15,
  author={Ostrovsky, Michael and Paes Leme, Renato},
  title={Gross substitutes and endowed assignment valuations},
  journal={Theoretical Economics},
  year=2015,
  volume={10},
  number={3},
  pages={853--865},
  url={https://econtheory.org/ojs/index.php/te/article/viewFile/20150853/13867/412}
}

@inproceedings{Mur96,
year={1996},
isbn={978-3-540-61310-7},
booktitle=ipco06,
volume={1084},
series=lncs,
title={Convexity and {S}teinitz's exchange property},
url={http://dx.doi.org/10.1007/3-540-61310-2_20},
publisher=springer,
author={Murota, Kazuo},
pages={260--274},
}

@article{MS99,
author = {Murota, Kazuo and Shioura, Akiyoshi},
title = {{M}-{C}onvex Function on Generalized Polymatroid},
journal = {Mathematics of Operations Research},
volume = {24},
number = {1},
pages = {95--105},
year = {1999},
URL = {http://dx.doi.org/10.1287/moor.24.1.95},
eprint = {http://dx.doi.org/10.1287/moor.24.1.95},
}

@article{FY03,
author = {Fujishige, Satoru and Yang, Zaifu},
title = {A Note on {K}elso and {C}rawford's {G}ross {S}ubstitutes Condition},
journal = {Mathematics of Operations Research},
volume = {28},
number = {3},
pages = {463--469},
year = {2003},
URL = {http://dx.doi.org/10.1287/moor.28.3.463.16393},
eprint = {http://dx.doi.org/10.1287/moor.28.3.463.16393},
}

@article{MT10,
title = "Characterization of the {W}alrasian equilibria of the assignment model ",
journal = "Journal of Mathematical Economics",
volume = "46",
number = "1",
pages = "6--20",
year = "2010",
issn = "0304-4068",
url = "http://www.sciencedirect.com/science/article/pii/S0304406809000627",
author = "Debasis Mishra and Dolf Talman",
}


@book{shalev2014book,
  title={Understanding Machine Learning: From Theory to Algorithms},
  author={Shalev-Shwartz, Shai and Ben-David, Shai},
  year=2014,
  publisher=cup
}

@article{BLN13,
  author    = {Ben-Zwi, Oren and
               Lavi, Ron and
               Newman, Ilan},
  title     = {Ascending auctions and Walrasian equilibrium},
  journal   = {CoRR},
  volume    = {abs/1301.1153},
  year      = {2013},
  url       = {http://arxiv.org/abs/1301.1153},
}


@article{ehrenfeucht1989general,
  title={A general lower bound on the number of examples needed for learning},
  author={Ehrenfeucht, Andrzej and Haussler, David and Kearns, Michael and Valiant, Leslie},
  journal={Information and Computation},
  volume={82},
  number={3},
  pages={247--261},
  year={1989},
  url={https://www.cis.upenn.edu/~mkearns/papers/lower.pdf},
  publisher={Elsevier},
}


@book{vapnik1982estimation,
  title={Estimation of dependences based on empirical data},
  author={Vapnik, Vladimir Naumovich and Kotz, Samuel},
  year={1982},
  publisher=springer,
}

@inproceedings{daniely2014multiclass,
  title={Optimal learners for multiclass problems},
  author={Daniely, Amit and Shalev-Shwartz, Shai},
  booktitle=colt14,
  pages={287--316},
  url={http://arxiv.org/abs/1405.2420},
  year={2014}
}

@techreport{littlestone1986compression,
  title={Relating data compression and learnability},
  author={Littlestone, Nick and Warmuth, Manfred},
  year={1986},
  url={https://users.soe.ucsc.edu/~manfred/pubs/lrnk-olivier.pdf},
  institution={University of California, Santa Cruz}
}

@article{murota1996valuated,
  title={Valuated matroid intersection {I}: Optimality criteria},
  author={Murota, Kazuo},
  journal={{SIAM} Journal on Discrete Mathematics},
  volume={9},
  number={4},
  pages={545--561},
  year={1996},
  url={http://www.keisu.t.u-tokyo.ac.jp/research/techrep/data/2003/METR03-42.pdf},
}

@article{ST15,
   author = {Shioura, Akiyoshi and Tamura, Akihisa},
   title = {Gross Substitutes Condition and Discrete Concavity for Multi-Unit
            Valuations: {A} Survey},
   journal = {Journal of the Operations Research Society of Japan},
   volume = {58},
   number = {1},
   year = 2015,
   pages = {61--103},
   url   = {http://www.orsj.or.jp/~archive/pdf/e_mag/Vol.58_01_061.pdf}
}

@Book{Matroid,
  Title                    = {Matroid Theory},
  Author                   = {Oxley, James G},
  Publisher                = {Oxford University Press},
  Year                     = {1997},
  Series                   = {Oxford Graduate Texts in Mathematics},
}

@inproceedings{elkind2007,
  title={Designing and learning optimal finite support auctions},
  author={Elkind, Edith},
  booktitle=ec07,
  pages={736--745},
  year={2007},
  url={http://eprints.soton.ac.uk/263443/1/finsup.pdf}
}

@inproceedings{medina2014learning,
  title={Learning Theory and Algorithms for revenue optimization in second price auctions with reserve},
  author={Medina, Andres Munoz and Mohri, Mehryar},
  booktitle=icml14,
  pages={262--270},
  year={2014},
  url={http://arxiv.org/abs/1310.5665}
}

@article{arrow1954existence,
  title={Existence of an equilibrium for a competitive economy},
  author={Arrow, Kenneth J and Debreu, Gerard},
  journal={Econometrica},
  pages={265--290},
  year={1954},
  url={http://web.stanford.edu/class/msande311/arrow-debreu.pdf}
}

@inproceedings{deng02complexity,
 author = {Deng, Xiaotie and Papadimitriou, Christos and Safra, Shmuel},
 title = {On the Complexity of Equilibria},
 booktitle = stoc02,
 year = {2002},
 isbn = {1-58113-495-9},
 pages = {67--71},
 numpages = {5},
 acmid = {509920},
 url={http://dl.acm.org/citation.cfm?id=509920}
} 

@article{nisan06communication,
	Author = {Nisan, Noam and Segal, Ilya},
	Issn = {0022-0531},
	Journal = jet,
	Keywords = {Distributional complexity},
	Number = {1},
	Pages = {192--224},
	Title = {The communication requirements of efficient allocations and supporting prices},
	Volume = {129},
	Year = {2006},
  url={http://web.stanford.edu/~isegal/prices.pdf}
	}

@inproceedings{DH09,
  title={The {Adwords} problem: {Online} keyword matching with budgeted bidders under random permutations},
  author={Devanur, Nikhil R and Hayes, Thomas P},
  booktitle=ec09,
  pages={71--78},
  year={2009},
  url={http://research.microsoft.com/en-us/um/people/nikdev/pubs/adwords.pdf}
}

@techreport{samplingbalcan07,
     title = {Random Sampling Auctions for Limited Supply},
     author = {Balcan, Maria-Florina and Devanur, Nikhil and
Hartline, Jason D and Talwar, Kunal},
     url = {http://reports-archive.adm.cs.cmu.edu/anon/2007/CMU-CS-07-154.pdf},
     year = {2007},
     institution = {Carnegie Mellon University},
     Date-Added = {09-01-2007},
}

@article{hanneke15,
  author    = {Hanneke, Steve},
  title     = {The Optimal Sample Complexity of {PAC} Learning},
  journal   = {CoRR},
  volume    = {abs/1507.00473},
  year      = {2015},
  url       = {http://arxiv.org/abs/1507.00473},
  timestamp = {Sun, 02 Aug 2015 18:42:02 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/Hanneke15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@book{pollard1984,
  title= "Convergence of stochastic processes",
  author={Pollard, David},
  year={1984},
  publisher={David Pollard},
  url = {http://www.stat.yale.edu/~pollard/Books/1984book/pollard1984.pdf},
}


@article{VC,
  title={On the uniform convergence of relative frequencies of events to their probabilities},
  author={Vapnik, Vladimir N and Chervonenkis, A Ya},
  journal={Theory of Probability \& Its Applications},
  volume={16},
  number={2},
  pages={264--280},
  year={1971},
  url={http://www.springer.com/cda/content/document/cda_downloaddocument/9783642411359-c1.pdf?SGWID=0-0-45-1431218-p175483535},
  publisher=siam
}


@book{AB,
 author = "Anthony, Martin and Bartlett, Peter L",
 title = {Neural Network Learning: Theoretical Foundations},
 year = {1999},
 publisher = cup,
}

@inproceedings{DNRR15,
year={2015},
isbn={978-3-662-48799-0},
booktitle=ascrypt15,
title={Pure Differential Privacy for Rectangle Queries via Private Partitions},
url={http://dx.doi.org/10.1007/978-3-662-48800-3_30},
publisher=springer,
author={Dwork, Cynthia and Naor, Moni and Reingold, Omer and Rothblum, Guy N},
pages={735--751},
}

@inproceedings{BartheO13,
  author    = {Barthe, Gilles and
               Olmedo, Federico},
  title     = {Beyond Differential Privacy: Composition Theorems and Relational Logic
               for $f$-divergences between Probabilistic Programs},
  booktitle = icalp13,
  series    = lncs,
  volume    = {7966},
  pages     = {49--60},
  publisher = springer,
  year      = {2013},
  url       = {http://certicrypt.gforge.inria.fr/2013.ICALP.pdf}
}

@inproceedings{DBLP:conf/stoc/DworkFHPRR15,
  author    = {Dwork, Cynthia and
               Feldman, Vitaly and
               Hardt, Moritz and
               Pitassi, Toniann and
               Reingold, Omer and
               Roth, Aaron},
  title     = {Preserving Statistical Validity in Adaptive Data Analysis},
  booktitle = stoc15,
  pages     = {117--126},
  year      = {2015},
  url       = {http://doi.acm.org/10.1145/2746539.2746580},
}
@inproceedings{xu:hal-00879140,
  TITLE = {Metrics for Differential Privacy in Concurrent Systems},
  AUTHOR = {Xu, Lili and Chatzikokolakis, Konstantinos and Lin, Huimin},
  URL = {https://hal.inria.fr/hal-00879140},
  BOOKTITLE = {IFIP International Conference on Formal Techniques for Distributed
    Objects, Components and Systems (FORTE), Berlin, Germany},
  EDITOR = {Erika Abraham and Catuscia Palamidessi},
  PUBLISHER = springer,
  SERIES = lncs,
  VOLUME = {8461},
  PAGES = {199--215},
  YEAR = {2014},
  MONTH = Jun,
  KEYWORDS = {differential privacy ; probabilistic automata ; bisimulation metrics ; verification},
  PDF = {https://hal.inria.fr/hal-00879140/file/forte-hal.pdf},
  HAL_ID = {hal-00879140},
  HAL_VERSION = {v2},
}

@InProceedings{ChakarovS14,
author = {Aleksandar Chakarov and Sriram Sankaranarayanan},
title = {Expectation Invariants as Fixed Points of Probabilistic Programs},
year = {2014},
pages = {85--100},
publisher = springer,
booktitle = sas14,
series = lncs,
volume = {8723},
url = {https://www.cs.colorado.edu/~srirams/papers/sas14-expectations.pdf}
}

@inproceedings{CousotM12,
  author    = {Patrick Cousot and
               Michael Monerau},
  title     = {Probabilistic Abstract Interpretation},
  booktitle = esop12,
  series    = lncs,
  volume    = {7211},
  pages     = {169--193},
  publisher = springer,
  year      = {2012},
  url       = {http://www.di.ens.fr/~cousot/publications.www/Cousot-Monerau-ESOP2012-extended.pdf}
}

@incollection{dwork2006our,
  title={Our data, ourselves: Privacy via distributed noise generation},
  author={Dwork, Cynthia and
          Kenthapadi, Krishnaram and
          {McSherry}, Frank and
          Mironov, Ilya and
          Naor, Moni},
  booktitle=eucrypt06,
  pages={486--503},
  year={2006},
  publisher=springer
}

@inproceedings{lyu2016understanding,
  title={Understanding the {Sparse Vector Technique} for Differential Privacy},
  author={Lyu, Min and Su, Dong and Li, Ninghui},
  booktitle=vldb17,
  volume=10,
  number=6,
  pages={637--648},
  url={http://arxiv.org/abs/1603.01699},
  year={2017},
}

@inproceedings{DBLP:journals/corr/OhV13,
  author    = {
    Peter Kairouz and 
    Sewoong Oh and
    Pramod Viswanath},
  title     = {The Composition Theorem for Differential Privacy},
  booktitle = icml15,
  pages     = {1376--1385},
  volume    = 37,
  series    = pmlr,
  url       = {https://arxiv.org/abs/1311.0776},
  year      = {2015},
  publisher = jmlr
}

@article{dwork2015reusable,
  title={The reusable holdout: Preserving validity in adaptive data analysis},
  author={Dwork, Cynthia and Feldman, Vitaly and Hardt, Moritz and Pitassi,
    Toniann and Reingold, Omer and Roth, Aaron},
  journal={Science},
  volume={349},
  number={6248},
  pages={636--638},
  year={2015},
  publisher={American Association for the Advancement of Science}
}

@article{aldous93shift,
    author = {Aldous, D. J. and Thorisson, H.},
    citeulike-article-id = {4046853},
    journal = {Stochastic Proc. Appl},
    keywords = {aldousbib},
    mrnumber = {1198659},
    pages = {1--14},
    posted-at = {2009-02-13 21:55:05},
    priority = {2},
    title = {{Shift-Coupling}},
    volume = {44},
    year = {1993}
}

@inproceedings{bubley1997path,
  title={Path coupling: {A} technique for proving rapid mixing in {M}arkov chains},
  author={Bubley, Russ and Dyer, Martin},
  booktitle=focs97,
  pages={223--231},
  year={1997},
}

@unpublished{DworkRothblumCDP,
  author    = {Cynthia Dwork and
               Guy N. Rothblum},
  title     = {Concentrated Differential Privacy},
  journal   = {CoRR},
  volume    = {abs/1603.01887},
  year      = {2016},
  url       = {http://arxiv.org/abs/1603.01887},
  timestamp = {Wed, 07 Jun 2017 14:40:05 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/DworkR16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{BunS2016,
  author = {Bun, Mark and Steinke, Thomas},
  title = {Concentrated Differential Privacy: Simplifications, Extensions, and Lower Bounds},
  archivePrefix = "arXiv",
  eprint = {1605.02065},
  primaryClass = "cs.CR",
  booktitle = tcc16b,
  pages={635--658},
  series  = lncs,
  year = {2016-B},
  volume = {9985},
  publisher = springer,
  url = {https://arxiv.org/abs/1605.02065},
}

@inproceedings{MironovRDP,
  title = {R\'enyi Differential Privacy},
  author  = {Ilya Mironov},
  year  = 2017,
  URL = {https://arxiv.org/abs/1702.07476},
  booktitle = csf17
}

@inproceedings{BunSU16,
  author = {Bun, Mark and Steinke, Thomas and Ullman, Jonathan},
  title = {Make Up Your Mind: The Price of Online Queries in Differential Privacy},
  booktitle = soda17,
  pages = {1306--1325},
  year = 2017,
  url = {https://arxiv.org/abs/1604.04618}
}

@inproceedings{moser2009constructive,
  title={A constructive proof of the {Lov{\'a}sz Local Lemma}},
  author={Moser, Robin A},
  booktitle=stoc09,
  pages={343--350},
  year={2009},
}

@inproceedings{micciancio1997oblivious,
  title={Oblivious data structures: {Applications} to cryptography},
  author={Micciancio, Daniele},
  booktitle=stoc97,
  pages={456--464},
  year={1997},
}

@inproceedings{jonsson1991specification,
  title={Specification and refinement of probabilistic processes},
  author={Jonsson, Bengt and Larsen, Kim Guldstrand},
  booktitle=lics91,
  pages={266--277},
  year={1991},
}

@inproceedings{rogers2016privacy,
  title={Privacy odometers and filters: Pay-as-you-go composition},
  author={Rogers, Ryan and Vadhan, Salil and Roth, Aaron and Ullman, Jonathan},
  booktitle=nips16,
  pages={1921--1929},
  year={2016},
  url={http://arxiv.org/abs/1605.08294}
}

@inproceedings{sousa2016cartesian,
  title={Cartesian {H}oare logic for verifying $k$-safety properties},
  author={Sousa, Marcelo and Dillig, Isil},
  booktitle=pldi16,
  pages={57--69},
  year={2016},
}

@inproceedings{BKOZ12-popl,
  title={Probabilistic relational reasoning for differential privacy},
  author={Barthe, Gilles and K{\"o}pf, Boris and Olmedo, Federico and
    Zanella B{\'e}guelin, Santiago},
  booktitle=popl12,
  volume={47},
  number={1},
  pages={97--110},
  year={2012},
}

@inproceedings{zhang2016autopriv,
 author = {Zhang, Danfeng and Kifer, Daniel},
 title = {{LightDP}: Towards Automating Differential Privacy Proofs},
 booktitle = popl17,
 year = {2017},
 pages = {888--901},
 url = {https://arxiv.org/abs/1607.08228},
} 


@article{JerrumS89,
  author    = {Mark Jerrum and
               Alistair Sinclair},
  title     = {Approximating the Permanent},
  journal   = siamjc,
  volume    = {18},
  number    = {6},
  pages     = {1149--1178},
  year      = {1989},
  url       = {http://dx.doi.org/10.1137/0218077},
  doi       = {10.1137/0218077},
  timestamp = {Mon, 12 Sep 2011 16:10:07 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/siamcomp/JerrumS89},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/rsa/Jerrum95,
  author    = {Mark Jerrum},
  title     = {A Very Simple Algorithm for Estimating the Number of
    $k$-Colorings of a Low-Degree Graph},
  journal   = {Random Structures and Algorithms},
  volume    = {7},
  number    = {2},
  pages     = {157--166},
  year      = {1995},
  url       = {http://dx.doi.org/10.1002/rsa.3240070205},
  doi       = {10.1002/rsa.3240070205},
  publisher = {Wiley},
  timestamp = {Sat, 14 Apr 2012 16:35:21 +0200},
  biburl    =
  {http://dblp.uni-trier.de/rec/bib/journals/rsa/Jerrum95},
  bibsource = {dblp computer science bibliography,
    http://dblp.org}
}

@inproceedings{Sato16,
  title = {Approximate Relational {H}oare Logic for Continuous Random Samplings},
  author = {Tetsuya Sato},
  booktitle = mfps16,
  pages = {277--298},
  year = 2016,
  volume = 325,
  url = {https://arxiv.org/abs/1603.01445},
  series = entcs,
  publisher = elsevier
}

@article{strassen1965existence,
  title={The existence of probability measures with given marginals},
  author={Strassen, Volker},
  journal={The Annals of Mathematical Statistics},
  pages={423--439},
  year={1965},
  publisher={Institute of Mathematical Statistics},
  url={http://projecteuclid.org/euclid.aoms/1177700153}
}

@inproceedings{tracolDZ11,
  author    = {Mathieu Tracol and
               Jos\'{e}e Desharnais and
               Abir Zhioua},
  title     = {Computing Distances between Probabilistic Automata},
  booktitle = {Workshop on Quantitative Aspects of Programming
               Languages ({QAPL}), Saarbr{\"{u}}cken, Germany},
  pages     = {148--162},
  year      = {2011},
  series    = eptcs,
  volume    = 57,
  publisher = {Open Publishing Association},
  url       = {http://dx.doi.org/10.4204/EPTCS.57.11},
  doi       = {10.4204/EPTCS.57.11},
  timestamp = {Mon, 28 Oct 2013 16:56:55 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1107-1206},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{desharnaisLT08, 
  author    = {Jos\'{e}e Desharnais and
               Fran\c{c}ois Laviolette and
               Mathieu Tracol},
  booktitle={International Conference on Quantitative Evaluation of Systems
    ({QEST}), Saint Malo, France}, 
  title={Approximate Analysis of Probabilistic Processes: Logic, Simulation and Games}, 
  year={2008}, 
  pages={264--273}, 
  publisher=ieee,
  doi={10.1109/QEST.2008.42}, 
  month=sep}

@inproceedings{LarsenS89,
  author    = {Larsen, Kim Guldstrand and
               Skou, Arne},
  title     = {Bisimulation Through Probabilistic Testing},
  booktitle = popl89,
  pages     = {344--352},
  year      = {1989},
  url       = {http://doi.acm.org/10.1145/75277.75307},
  timestamp = {Mon, 21 May 2012 16:19:51 +0200}, biburl    = {http://dblp.uni-trier.de/rec/bib/conf/popl/LarsenS89},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{giacalone1990algebraic,
  title={Algebraic reasoning for probabilistic concurrent systems},
  author={Giacalone, Alessandro and Jou, Chi-Chang and Smolka, Scott A.},
  booktitle={{IFIP} {TC2} Working Conference on Programming Concepts and Methods},
  year={1990},
}

@inproceedings{SegalaTurrini07, 
  author={Roberto Segala and Andrea Turrini}, 
  booktitle=csf07, 
  title={Approximated Computationally Bounded Simulation Relations for Probabilistic Automata}, 
  year={2007}, 
  pages={140--156}, 
  doi={10.1109/CSF.2007.8}, 
  ISSN={1063-6900}, 
  month=jul
}

@phdthesis{OlmedoThesis,
  title        = {Approximate Relational Reasoning for Probabilistic Programs},
  author       = {Federico Olmedo},
  school       = {Universidad Polit\'ecnica de Madrid},
  year         = {2014},
  url          = {http://software.imdea.org/~federico/thesis.pdf}
}

@article{DBLP:journals/jct/AharoniBGPS11,
  author    = {Ron Aharoni and
               Eli Berger and
               Agelos Georgakopoulos and
               Amitai Perlstein and
               Philipp Spr{\"{u}}ssel},
  title     = {The Max-Flow Min-Cut theorem for countable networks},
  journal   = {Journal of Combinatorial Theory, Series B},
  volume    = {101},
  number    = {1},
  pages     = {1--17},
  year      = {2011},
  url       = {http://dx.doi.org/10.1016/j.jctb.2010.08.002},
  doi       = {10.1016/j.jctb.2010.08.002},
  timestamp = {Sat, 04 Dec 2010 15:33:06 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jct/AharoniBGPS11},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{katsumata2015codensity,
  title={Codensity Liftings of Monads},
  author={Katsumata, Shin-ya and Sato, Tetsuya},
  booktitle= calco15,
  series    = lipics,
  pages ={156--170},
  year    = 2015,
  publisher = dagstuhl,
  volume={35},
}

@inproceedings{aldous1983random,
  title={Random walks on finite groups and rapidly mixing Markov chains},
  author={Aldous, David},
  booktitle={S{\'e}minaire de Probabilit{\'e}s {XVII} 1981/82},
  pages={243--297},
  series=lnm,
  volume=986,
  year={1983},
  publisher=springer
}

@book {RudinPMA,
  AUTHOR = {Rudin, Walter},
  TITLE = {Principles of mathematical analysis},
  EDITION = {Third},
  SERIES = {International Series in Pure and Applied Mathematics},
  PUBLISHER = mcgh,
  YEAR = {1976},
  PAGES = {x+342},
  MRCLASS = {26-02},
  MRNUMBER = {0385023},
}

@inproceedings{adafuzz,
  title={A framework for adaptive differential privacy},
  author={Winograd-Cort, Daniel and
          Haeberlen, Andreas and
          Roth, Aaron and
          Pierce, Benjamin C.},
  booktitle= icfp17,
  year    = 2017
}

@book{Kleinberg:2005:AD:1051910,
 author = {Kleinberg, Jon and Tardos, Eva},
 title = {Algorithm Design},
 year = {2005},
 isbn = {0321295358},
 publisher = aw,
 address = {Boston, MA, USA},
} 

@inproceedings{bornholt2016optimizing,
  title={Optimizing synthesis with metasketches},
  author={Bornholt, James and Torlak, Emina and Grossman, Dan and Ceze, Luis},
  booktitle=popl16,
  pages={775--788},
  year={2016},
}

@inproceedings{dwork2009complexity,
  title={On the complexity of differentially private data release: efficient algorithms and hardness results},
  author={Dwork, Cynthia and Naor, Moni and Reingold, Omer and Rothblum, Guy N and Vadhan, Salil},
  booktitle=stoc09,
  pages={381--390},
  year={2009},
}

@inproceedings{graf1997construction,
  title={Construction of abstract state graphs with PVS},
  author={Graf, Susanne and Sa{\"\i}di, Hassen},
  booktitle=cav97,
  pages={72--83},
  year={1997},
  organization=springer
}

@inproceedings{alur2013syntax,
  title={Syntax-guided synthesis},
  author={Alur, Rajeev and Bodik, Rastislav and Juniwal, Garvit and Martin, Milo MK and Raghothaman, Mukund and Seshia, Sanjit A and Singh, Rishabh and Solar-Lezama, Armando and Torlak, Emina and Udupa, Abhishek},
  booktitle={Formal Methods in Computer-Aided Design {(FMCAD)}, Portland, Oregon},
  pages={1--8},
  year={2013},
  organization={IEEE}
}

@inproceedings{hojjat2012verification,
  title={A verification toolkit for numerical transition systems},
  author={Hojjat, Hossein and Kone{\v{c}}n{\`y}, Filip and Garnier, Florent and Iosif, Radu and Kuncak, Viktor and R{\"u}mmer, Philipp},
  booktitle=fm12,
  pages={247--251},
  year={2012},
  organization=springer
}

@techreport{mcmillan2013solving,
  title={Solving constrained {H}orn clauses using interpolation},
  author={McMillan, Kenneth L and Rybalchenko, Andrey},
  number={MSR-TR-2013-6},
  institution={Microsoft Research},
  year={2013}
}

@inproceedings{beyer2009software,
  title={Software model checking via large-block encoding},
  author={Beyer, Dirk and Cimatti, Alessandro and Griggio, Alberto and Keremoglu, M Erkan and Sebastiani, Roberto},
  booktitle={Formal Methods in Computer-Aided Design {(FMCAD)}, Austin, Texas},
  pages={25--32},
  year={2009},
  organization={IEEE}
}

@inproceedings{mathsat,
  title={The MathSAT5 SMT Solver.},
  author={Cimatti, Alessandro and Griggio, Alberto and Schaafsma, Bastiaan Joost and Sebastiani, Roberto},
  booktitle=tacas13,
  volume={7795},
  pages={93--107},
  year={2013},
  organization=springer
}


@inproceedings{grebenshchikov2012hsf,
  title={{HSF (C)}: {A} software verifier based on {H}orn clauses},
  author={Grebenshchikov, Sergey and Gupta, Ashutosh and Lopes, Nuno P and Popeea, Corneliu and Rybalchenko, Andrey},
  booktitle=tacas12,
  pages={549--551},
  year={2012},
  organization=springer
}


@inproceedings{grebenshchikov2012,
 author = {Grebenshchikov, Sergey and Lopes, Nuno P. and Popeea, Corneliu and Rybalchenko, Andrey},
 title = {Synthesizing Software Verifiers from Proof Rules},
 booktitle = pldi12,
 year = {2012},
 isbn = {978-1-4503-1205-9},
 location = {Beijing, China},
 pages = {405--416},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/2254064.2254112},
 doi = {10.1145/2254064.2254112},
 acmid = {2254112},
 keywords = {proof rules, software model checking, software verification, verification tool synthesis},
}


@inproceedings{gurfinkel2015seahorn,
  title={{SeaHorn}: {A} Framework for Verifying {C} Programs (Competition Contribution).},
  author={Gurfinkel, Arie and Kahsai, Temesghen and Navas, Jorge A},
  booktitle=tacas15,
  pages={447--450},
  year={2015}
}

@inproceedings{hoder2011muz,
  title={$\mu${Z}-An Efficient Engine for Fixed Points with Constraints.},
  author={Hoder, Krystof and Bj{\o}rner, Nikolaj and de Moura, Leonardo Mendon{\c{c}}a},
  booktitle=cav11,
  pages={457--462},
  year={2011},
  organization=springer
}

@inproceedings{DBLP:conf/asplos/Solar-LezamaTBSS06,
  author    = {Armando Solar{-}Lezama and
      Liviu Tancau and
      Rastislav Bod{\'{\i}}k and
      Sanjit A. Seshia and
      Vijay A.  Saraswat},
  title     = {Combinatorial sketching for finite programs},
  booktitle = asplos06,
  pages     = {404--415},
  year      = {2006},
  url       = {http://doi.acm.org/10.1145/1168857.1168907},
  doi       = {10.1145/1168857.1168907},
  timestamp = {Tue, 15 May 2007 09:22:32 +0200},
  biburl    =
  {http://dblp.dagstuhl.de/rec/bib/conf/asplos/Solar-LezamaTBSS06},
  bibsource = {dblp computer science bibliography,
    http://dblp.org}
}

@article{pnueli1998translation,
  title={Translation validation},
  author={Pnueli, Amir and Siegel, Michael and Singerman, Eli},
  journal=tacas98,
  pages={151--166},
  year={1998},
  publisher=springer
}

@inproceedings{necula2000translation,
  title={Translation validation for an optimizing compiler},
  author={Necula, George C},
  booktitle=pldi00,
  volume={35},
  number={5},
  pages={83--94},
  year={2000},
}

@inproceedings{kopf2010approximation,
  title={Approximation and randomization for quantitative information-flow analysis},
  author={K{\"o}pf, Boris and Rybalchenko, Andrey},
  booktitle=csf10,
  pages={3--14},
  year={2010},
}

@inproceedings{Srivastava10,
 author = {Srivastava, Saurabh and Gulwani, Sumit and Foster, Jeffrey S.},
 title = {From Program Verification to Program Synthesis},
 booktitle = popl10,
 year = {2010},
 isbn = {978-1-60558-479-9},
 location = {Madrid, Spain},
 pages = {313--326},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/1706299.1706337},
 doi = {10.1145/1706299.1706337},
 acmid = {1706337},
 address = {New York, NY, USA},
 keywords = {proof-theoretic program synthesis, verification},
}

@inproceedings{Beyene14,
 author = {Beyene, Tewodros and Chaudhuri, Swarat and Popeea, Corneliu and Rybalchenko, Andrey},
 title = {A Constraint-based Approach to Solving Games on Infinite Graphs},
 booktitle = popl14,
 year = {2014},
 isbn = {978-1-4503-2544-8},
 location = {San Diego, California, USA},
 pages = {221--233},
 numpages = {13},
 acmid = {2535860},
 address = {New York, NY, USA},
 keywords = {games, horn clauses, program synthesis, proof rules, reactive synthesis, static analysis},
}

@inproceedings{beyene2013solving,
  title={Solving existentially quantified {H}orn clauses},
  author={Beyene, Tewodros A and Popeea, Corneliu and Rybalchenko, Andrey},
  booktitle=cav13,
  pages={869--882},
  year={2013},
  organization=springer
}

@inproceedings{gulwani2011synthesis,
  title={Synthesis of loop-free programs},
  author={Sumit Gulwani and Susmit Jha and Ashish Tiwari and Ramarathnam Venkatesan},
  booktitle=pldi11,
  year={2011}
}

@inproceedings{lahiri2006smt,
  title={{SMT} techniques for fast predicate abstraction},
  author={Lahiri, Shuvendu K and Nieuwenhuis, Robert and Oliveras, Albert},
  booktitle=cav06,
  pages={424--437},
  year={2006},
  organization=springer
}

@incollection{bjorner2015horn,
  title={Horn clause solvers for program verification},
  author={Bj{\o}rner, Nikolaj and Gurfinkel, Arie and McMillan, Ken and Rybalchenko, Andrey},
  booktitle={Fields of Logic and Computation {II}},
  pages={24--51},
  year={2015},
  publisher=springer
}

@inproceedings{MacQueenPS84,
  author    = {David B. MacQueen and
               Gordon D. Plotkin and
               Ravi Sethi},
  editor    = {Ken Kennedy and
               Mary S. Van Deusen and
               Larry Landweber},
  title     = {An Ideal Model for Recursive Polymorphic Types},
  booktitle = popl84,
  pages     = {165--174},
  year      = {1984},
  url       = {http://doi.acm.org/10.1145/800017.800528},
  doi       = {10.1145/800017.800528},
  timestamp = {Mon, 21 May 2012 16:19:51 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/popl/MacQueenPS84},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{AbadiP90,
  author    = {Mart{\'{\i}}n Abadi and
               Gordon D. Plotkin},
  title     = {A Per Model of Polymorphism and Recursive Types},
  booktitle = lics90,
  pages     = {355--365},
  year      = {1990},
  url       = {https://doi.org/10.1109/LICS.1990.113761},
  doi       = {10.1109/LICS.1990.113761},
  timestamp = {Thu, 25 May 2017 00:42:41 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/lics/AbadiP90},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{Shamir16,
  author    = {Ohad Shamir},
  title     = {Without-Replacement Sampling for Stochastic Gradient Methods: Convergence
               Results and Application to Distributed Optimization},
  journal   = {CoRR},
  volume    = {abs/1603.00570},
  year      = {2016},
  url       = {http://arxiv.org/abs/1603.00570},
  timestamp = {Sat, 02 Apr 2016 11:49:48 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/Shamir16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}


@book{jansen2013analyzing,
  author    = {Thomas Jansen},
  title     = {Analyzing Evolutionary Algorithms: The Computer Science Perspective},
  series    = {Natural Computing Series},
  publisher = springer,
  year      = {2013},
  url       = {https://doi.org/10.1007/978-3-642-17339-4},
  doi       = {10.1007/978-3-642-17339-4},
  isbn      = {978-3-642-17338-7},
  timestamp = {Tue, 16 May 2017 14:24:38 +0200},
  biburl    =
  {http://dblp2.uni-trier.de/rec/bib/series/ncs/Jansen13},
  bibsource = {dblp computer science bibliography,
    http://dblp.org}
}


@book{HartlC,
author={Daniel L. Hartl and Andrew G. Clark},
title={Principles of Population Genetics},
edition={Fourth},
publisher={Sinauer Associates},
year={2006}}

@article{BousquetE02,
  author    = {Olivier Bousquet and
               Andr{\'{e}} Elisseeff},
  title     = {Stability and Generalization},
  journal   = jmlr,
  volume    = {2},
  pages     = {499--526},
  year      = {2002},
  url       = {http://www.jmlr.org/papers/v2/bousquet02a.html}
}

@inproceedings{GomulkiewiczKK03,
  author    = {Marcin Gomulkiewicz and
               Marek Klonowski and
               Miroslaw Kutylowski},
  title     = {Rapid Mixing and Security of {C}haum's Visual Electronic Voting},
  booktitle = esorics03,
  series    = lncs,
  volume    = {2808},
  pages     = {132--145},
  publisher = springer,
}

@inproceedings{BizjakB15,
  author    = {Ales Bizjak and
               Lars Birkedal},
  title     = {Step-Indexed Logical Relations for Probability},
  booktitle = fossacs15,
  series    = lncs,
  volume    = {9034},
  pages     = {279--294},
  publisher = springer,
  year      = {2015}
}

@inproceedings{SangiorgiV16,
  author    = {Davide Sangiorgi and
               Valeria Vignudelli},
  title     = {Environmental bisimulations for probabilistic higher-order languages},
  booktitle = popl16,
  pages     = {595--607},
  year      = {2016}
}

@inproceedings{DallagoSA14,
  author    = {Ugo Dal Lago and
               Davide Sangiorgi and
               Michele Alberti},
  title     = {On coinductive equivalences for higher-order probabilistic functional
               programs},
  booktitle = popl14,
  pages     = {297--308},
  year      = {2014}
}

@article{dixit2012finite,
  title={A finite population model of molecular evolution: {T}heory and computation},
  author={Dixit, Narendra M and Srivastava, Piyush and Vishnoi, Nisheeth K},
  journal={Journal of Computational Biology},
  volume={19},
  number={10},
  pages={1176--1202},
  year={2012},
  publisher={Mary Ann Liebert}
}

@phdthesis{Hartog:thesis,
	Author = {den Hartog, J.},
	School = {Vrije Universiteit Amsterdam},
	Title = {Probabilistic extensions of semantical models},
	Year = {2002}}

@article{CanteautFNPRV12,
  author    = {Anne Canteaut and
               Thomas Fuhr and
               Mar{\'{\i}}a Naya{-}Plasencia and
               Pascal Paillier and
               Jean{-}Ren{\'{e}} Reinhard and
               Marion Videau},
  title     = {A Unified Indifferentiability Proof for Permutation- or Block Cipher-Based
               Hash Functions},
  journal   = {{IACR} Cryptology ePrint Archive},
  volume    = {2012},
  pages     = {363},
  year      = {2012},
  url       = {http://eprint.iacr.org/2012/363},
  timestamp = {Fri, 28 Mar 2014 20:49:29 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/iacr/CanteautFNPRV12},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{NanevskiBG11,
  author    = {Aleksandar Nanevski and
               Anindya Banerjee and
               Deepak Garg},
  title     = {Verification of Information Flow and Access Control Policies with
               Dependent Types},
  booktitle = sandp11,
  pages     = {165--179},
  year      = {2011}
}


@inproceedings{GhaniFS16,
  author    = {Neil Ghani and
               Fredrik Nordvall Forsberg and
               Alex Simpson},
  title     = {Comprehensive Parametric Polymorphism: {C}ategorical Models and Type
               Theory},
  booktitle = fossacs16,
  series    = lncs,
  volume    = {9634},
  pages     = {3--19},
  publisher = springer,
  year      = {2016}
}



@article{aldous93shift,
    author = {Aldous, D. J. and Thorisson, H.},
    citeulike-article-id = {4046853},
    journal = {Stochastic Processes and their Applications},
    keywords = {aldousbib},
    mrnumber = {1198659},
    pages = {1--14},
    posted-at = {2009-02-13 21:55:05},
    priority = {2},
    title = {Shift-Coupling},
    volume = {44},
    year = {1993}
}

@book {LevinPW09,
AUTHOR = {Levin, David A. and Peres, Yuval and Wilmer, Elizabeth L.},
TITLE = {Markov chains and mixing times},
PUBLISHER = {American Mathematical Society},
YEAR = {2009}
}

@book{Villani08,
  title={Optimal transport: {O}ld and new},
  author={Villani, C{\'e}dric},
  year={2008},
  publisher=springer
}

@inproceedings{BentonHN13,
  author    = {Nick Benton and
               Martin Hofmann and
               Vivek Nigam},
  title     = {Proof-Relevant Logical Relations for Name Generation},
  booktitle = tlca13,
  series    = lncs,
  volume    = {7941},
  pages     = {48--60},
  publisher = springer,
  year      = {2013}
}


@inproceedings{KrishnaswamiB11,
  author    = {Neelakantan R. Krishnaswami and
               Nick Benton},
  title     = {Ultrametric Semantics of Reactive Programs},
  booktitle = lics11,
  pages     = {257--266},
  year      = {2011}}


@inproceedings{BeringerH07,
  author    = {Lennart Beringer and
               Martin Hofmann},
  title     = {Secure information flow and program logics},
  booktitle = csf07,
  pages     = {233--248},
  year      = {2007}
}
@inproceedings{LahiriHKR12,
  author    = {Shuvendu K. Lahiri and
               Chris Hawblitzel and
               Ming Kawaguchi and
               Henrique Reb{\^{e}}lo},
  title     = {{SYMDIFF}: {A} Language-Agnostic Semantic Diff Tool for Imperative
               Programs},
  booktitle = cav12,
  series    = lncs,
  volume    = {7358},
  pages     = {712--717},
  publisher = springer,
  year      = {2012}
}


@inproceedings{LahiriMSH13,
  author    = {Shuvendu K. Lahiri and
               Kenneth L. McMillan and
               Rahul Sharma and
               Chris Hawblitzel},
  title     = {Differential assertion checking},
  booktitle = esecfse13,
  pages     = {345--355},
  year      = {2013}
}

@article{BartheCK16,
author={Gilles Barthe and Juan Manuel Crespo and C{\'{e}}sar Kunz},
title={Product programs and relational program logics},
journal={Journal of Logical and Algebraic Methods in Programming},
year={2016}}


@InProceedings{DHS05:spc,
  author =       "Adam Darvas and Reiner H{\"{a}}hnle and David Sands",
  title =        "A Theorem Proving Approach to Analysis of Secure
                 Information Flow",
  booktitle =    "Security in Pervasive Computing",
  pages =        "193--209",
  year =         "2005",
  volume =       "3450",
  series =       lncs,
  publisher =    springer,
  note =         "Preliminary version in the informal proceedings of WITS 2003"
}

@inproceedings{MisailovicRR11,
  author    = {Sasa Misailovic and
               Daniel M. Roy and
               Martin C. Rinard},
  title     = {Probabilistically Accurate Program Transformations},
  booktitle = sas11,
  series    = lncs,
  volume    = {6887},
  pages     = {316--333},
  publisher = springer,
  year      = {2011}
}

@inproceedings{LogozzoLFB14,
  author    = {Francesco Logozzo and
               Shuvendu K. Lahiri and
               Manuel F{\"{a}}hndrich and
               Sam Blackshear},
  title     = {Verification modulo versions: {T}owards usable verification},
  booktitle = pldi14,
  pages     = {32},
  year      = {2014}
}

@article{GodlinS13,
  author    = {Benny Godlin and
               Ofer Strichman},
  title     = {Regression verification: {P}roving the equivalence of similar programs},
  journal   = {Software Testing, Verification, and Reliability},
  volume    = {23},
  number    = {3},
  pages     = {241--258},
  year      = {2013}
}



@inproceedings{PartushY14,
  author    = {Nimrod Partush and
               Eran Yahav},
  title     = {Abstract semantic differencing via speculative correlation},
  booktitle = oopsla14,
  pages     = {811--828},
  year      = {2014}
}

@inproceedings{PersonDEP08,
 author = {Person, Suzette and Dwyer, Matthew B. and Elbaum, Sebastian and P\v{a}s\v{a}reanu, Corina S.},
 title = {Differential Symbolic Execution},
 booktitle = fse08,
 year = {2008},
 pages = {226--237},
}

@inproceedings{DBLP:conf/esop/FosterKMR016,
  author    = {Nate Foster and
               Dexter Kozen and
               Konstantinos Mamouras and
               Mark Reitblatt and
               Alexandra Silva},
  title     = {Probabilistic {NetKAT}},
  booktitle = esop16,
  series    = lncs,
  volume    = {9632},
  pages     = {282--309},
  publisher = springer,
  year      = {2016},
  url       = {http://dx.doi.org/10.1007/978-3-662-49498-1_12},
  doi       = {10.1007/978-3-662-49498-1_12},
  timestamp = {Tue, 22 Mar 2016 15:54:03 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/esop/FosterKMR016},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{KaminskiKMO16,
  author    = {Benjamin Lucien Kaminski and
               Joost{-}Pieter Katoen and
               Christoph Matheja and
               Federico Olmedo},
  title     = {Weakest Precondition Reasoning for Expected Run-Times of Probabilistic
               Programs},
  booktitle = esop16,
  series    = lncs,
  volume    = {9632},
  pages     = {364--389},
  publisher = springer,
  year      = {2016},
  url       = {http://dx.doi.org/10.1007/978-3-662-49498-1_15},
  doi       = {10.1007/978-3-662-49498-1_15},
  timestamp = {Tue, 22 Mar 2016 15:54:03 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/esop/KaminskiKMO16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@InProceedings{ABB06:popl,
  author =       "Torben Amtoft and Sruthi Bandhakavi and Anindya Banerjee",
  title =        "A logic for information flow in object-oriented
                 programs",
  booktitle =    popl06,
  year =         "2006",
  pages =        "91--102",
}

@article{DBLP:journals/iacr/BartheDFGSS16,
  author    = {Gilles Barthe and
               Fran{\c{c}}ois Dupressoir and
               Sebastian Faust and
               Benjamin Gr{\'{e}}goire and
               Fran{\c{c}}ois{-}Xavier Standaert and
               Pierre{-}Yves Strub},
  title     = {Parallel Implementations of Masking Schemes and the Bounded Moment
               Leakage Model},
  journal   = {{IACR} Cryptology ePrint Archive},
  volume    = {2016},
  pages     = {912},
  year      = {2016},
  url       = {http://eprint.iacr.org/2016/912},
  timestamp = {Fri, 14 Oct 2016 13:36:12 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/iacr/BartheDFGSS16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/tcad/EldibWTS15,
  author    = {Hassan Eldib and
               Chao Wang and
               Mostafa M. I. Taha and
               Patrick Schaumont},
  title     = {Quantitative Masking Strength: {Q}uantifying the Power Side-Channel
               Resistance of Software Code},
  journal   = {{IEEE} Transansactions on {CAD} of Integrated Circuits and Systems},
  volume    = {34},
  number    = {10},
  pages     = {1558--1568},
  year      = {2015},
  url       = {http://dx.doi.org/10.1109/TCAD.2015.2424951},
  doi       = {10.1109/TCAD.2015.2424951},
  timestamp = {Thu, 03 Nov 2016 07:24:15 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/tcad/EldibWTS15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/crypto/IshaiSW03,
  author    = {Yuval Ishai and
               Amit Sahai and
               David Wagner},
  title     = {Private Circuits: {S}ecuring Hardware against Probing Attacks},
  booktitle = crypto03,
  series    = lncs,
  volume    = {2729},
  pages     = {463--481},
  publisher = springer,
  year      = {2003},
  url       = {http://dx.doi.org/10.1007/978-3-540-45146-4_27},
  doi       = {10.1007/978-3-540-45146-4_27},
  timestamp = {Tue, 05 Jul 2011 11:03:56 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/crypto/IshaiSW03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}


@inproceedings{Beringer11,
  author    = {Lennart Beringer},
  title     = {Relational Decomposition},
  booktitle = itp11,
  series    = lncs,
  volume    = {6898},
  pages     = {39--54},
  publisher = springer,
  year      = {2011}
}
@inproceedings{MullerKS15,
  author    = {Christian M{\"{u}}ller and
               M{\'{a}}t{\'{e}} Kov{\'{a}}cs and
               Helmut Seidl},
  title     = {An Analysis of Universal Information Flow Based on Self-Composition},
  booktitle = csf15,
  pages     = {380--393},
  year      = {2015}
}


@inproceedings{KovacsSF13,
  author    = {M{\'{a}}t{\'{e}} Kov{\'{a}}cs and
               Helmut Seidl and
               Bernd Finkbeiner},
  title     = {Relational abstract interpretation for the verification of 
               2-hypersafety properties},
  booktitle = ccs13,
  pages     = {211--222},
  year      = {2013}
}

@article{ElisseeffEP05,
  author    = {Andr{\'{e}} Elisseeff and
               Theodoros Evgeniou and
               Massimiliano Pontil},
  title     = {Stability of Randomized Learning Algorithms},
  journal   = jmlr,
  volume    = {6},
  pages     = {55--79},
  year      = {2005},
  url       = {http://www.jmlr.org/papers/v6/elisseeff05a.html},
  timestamp = {Wed, 21 Feb 2007 09:15:37 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jmlr/ElisseeffEP05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{PanageasSV16,
  author    = {Ioannis Panageas and
               Piyush Srivastava and
               Nisheeth K. Vishnoi},
  title     = {Evolutionary Dynamics in Finite Populations Mix Rapidly},
  booktitle = soda16,
  pages     = {480--497},
  year      = {2016},
  url       = {http://dx.doi.org/10.1137/1.9781611974331.ch36},
  doi       = {10.1137/1.9781611974331.ch36},
  timestamp = {Thu, 07 Apr 2016 12:20:54 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/soda/PanageasSV16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{Vishnoi15,
  author    = {Nisheeth K. Vishnoi},
  title     = {The Speed of Evolution},
  booktitle = soda15,
  pages     = {1590--1601},
  year      = {2015},
  url       = {http://dx.doi.org/10.1137/1.9781611973730.105},
  doi       = {10.1137/1.9781611973730.105},
  timestamp = {Wed, 28 Jan 2015 11:43:18 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/soda/Vishnoi15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{diaconis91,
    author = {Diaconis, Persi and Stroock, Daniel},
    citeulike-article-id = {8906755},
    citeulike-linkout-0 = {http://dx.doi.org/10.1214/aoap/1177005980},
    doi = {10.1214/aoap/1177005980},
    issn = {1050-5164},
    journal = {The Annals of Applied Probability},
    keywords = {eigenvalues, markov, rapid-mixing},
    month = feb,
    number = {1},
    pages = {36--61},
    posted-at = {2011-03-01 12:39:26},
    priority = {4},
    title = {Geometric Bounds for Eigenvalues of {M}arkov Chains},
    url = {http://dx.doi.org/10.1214/aoap/1177005980},
    volume = {1},
    year = {1991}
}


@article{JerrumS89,
  author    = {Mark Jerrum and
               Alistair Sinclair},
  title     = {Approximating the Permanent},
  journal   = siamjc,
  volume    = {18},
  number    = {6},
  pages     = {1149--1178},
  year      = {1989},
  url       = {http://dx.doi.org/10.1137/0218077},
  doi       = {10.1137/0218077},
  timestamp = {Mon, 12 Sep 2011 16:10:07 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/siamcomp/JerrumS89},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/rsa/KumarR01,
  author    = {V. S. Anil Kumar and H. Ramesh},
  title     = {Coupling vs. conductance for the {J}errum-{S}inclair chain},
  journal   = {Random Structures and Algorithms},
  volume    = {18},
  number    = {1},
  pages     = {1--17},
  year      = {2001},
  url       = {http://hariharan-ramesh.com/papers/mcmc.pdf},
  publisher = {Wiley}
}

@inproceedings{HardtRS16,
  author    = {Moritz Hardt and
               Ben Recht and
               Yoram Singer},
  title     = {Train faster, generalize better: {S}tability of stochastic gradient descent},
  booktitle = icml16,
  series    = jmlr,
  volume    = {48},
  pages     = {1225--1234},
  publisher = {JMLR.org},
  year      = {2016},
  url       = {http://jmlr.org/proceedings/papers/v48/hardt16.html},
  
}

@techreport{randomwalk:notes,
  author = {Avena, Luca and
            Heydenreich, Markus and
            den Hollander, Frank and
            Verbitskiy, Evgeny and
            van Zuijlen, Willem},
  title  = {Random Walks (lecture notes)},
  url    = {http://websites.math.leidenuniv.nl/probability/lecturenotes/RandomWalks.pdf},
  institution = {Mathematical Institute, Leiden University}
}

@book{vanbreugel,
author={Franck van Breugel},
title={Comparative Metric Semantics of Programming Languages:
Nondeterminism and Recursion},
series={Progress in Theoretical Computer Science},
publisher={Birkhauser},
year={1997}}

@inproceedings{DeBakkerZ82,
  author    = {J. W. de Bakker and
               Jeffery I. Zucker},
  editor    = {Harry R. Lewis and
               Barbara B. Simons and
               Walter A. Burkhard and
               Lawrence H. Landweber},
  title     = {Denotational Semantics of Concurrency},
  booktitle = stoc82,
  pages     = {153--158},
  year      = {1982},
  url       = {http://doi.acm.org/10.1145/800070.802188},
  doi       = {10.1145/800070.802188},
  timestamp = {Sun, 21 May 2017 00:22:29 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/stoc/DeBakkerZ82},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{ArnoldN80,
  author    = {Andr{\'{e}} Arnold and
               Maurice Nivat},
  title     = {Metric Interpretations of Infinite Trees and Semantics of non Deterministic
               Recursive Programs},
  journal   = tcs,
  volume    = {11},
  pages     = {181--205},
  year      = {1980},
  url       = {https://doi.org/10.1016/0304-3975(80)90045-6},
  doi       = {10.1016/0304-3975(80)90045-6},
  timestamp = {Sun, 28 May 2017 13:20:08 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/tcs/ArnoldN80},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@book{brooks2011handbook,
  title={Handbook of {M}arkov Chain {M}onte {C}arlo},
  author={Brooks, Steve and Gelman, Andrew and Jones, Galin and Meng,
    Xiao-Li},
  year={2011},
  publisher={CRC press}
}

@inproceedings{sato2016approximate,
  title={Approximate Relational {H}oare Logic for Continuous Random Samplings},
  author={Sato, Tetsuya},
  booktitle=mfps16,
  year={2016},
  url={http://arxiv.org/abs/1603.01445}
}

@article{metropolis1953equation,
  title={Equation of state calculations by fast computing machines},
  author={Metropolis, Nicholas and Rosenbluth, Arianna W and Rosenbluth,
    Marshall N and Teller, Augusta H and Teller, Edward},
  journal={The Journal of Chemical Physics},
  volume={21},
  number={6},
  pages={1087--1092},
  year={1953},
  publisher={AIP Publishing}
}

@inproceedings{Kozen16,
  author="Dexter Kozen",
  title="Kolmogorov Extension, Martingale Convergence, and Compositionality of Processes",
  booktitle=lics16,
  url = {http://hdl.handle.net/1813/41517},
  year={2016}
}

@book{durrett2008probability,
  title={Probability Models for {DNA} Sequence Evolution},
  author={Durrett, R.},
  isbn={9780387781693},
  lccn={2008929756},
  series={Probability and Its Applications},
  year={2008},
  publisher=springer
}

@article{Smyth:82,
  added-at = {2007-11-03T00:18:07.000+0100},
  author = {Smyth, Michael B. and Plotkin, Gordon D.},
  biburl = {http://www.bibsonomy.org/bibtex/2463c71fb3a6d5f453c9ced9044fcec7f/bsmyth},
  date = {2002-01-03},
  description = {dblp},
  interhash = {fa163d46ad9a635a36f162a6961931ad},
  intrahash = {463c71fb3a6d5f453c9ced9044fcec7f},
  journal = siamjc,
  number = 4,
  pages = {761--783},
  timestamp = {2007-11-03T00:18:21.000+0100},
  title = {The Category-Theoretic Solution of Recursive Domain Equations},
  url = {http://dblp.uni-trier.de/db/journals/siamcomp/siamcomp11.html#SmythP82},
  volume = 11,
  year = 1982
}

@inproceedings{Freyd1991,
author="Freyd, Peter",
title="Algebraically complete categories",
booktitle=ct90,
year="1990",
publisher=springer,
series={Lecture Notes in Mathematics},
volume=1488,
pages="95--104",
isbn="978-3-540-46435-8",
url="http://dx.doi.org/10.1007/BFb0084215"
}

@article{Lawvere:02,
  author    = {William F. Lawvere},
  title     = {Metric Spaces, Generalized Logic, and Closed Categories},
  journal   = {Reprints in Theory and Applications of Categories},
  volume    = {1},
  pages     = {1--37},
  note      = {Originally published in ``Rendiconti del seminario matematico e fisico di Milano, XLIII (1973), 135-166''},
  year      = {2002}
}

@book{Monoidal,
  editor    = {Hofmann, Dirk and Seal, Gavin J. and Tholen, Walter},
  title     = {Monoidal Topology},
  publisher = cup,
  year      = {2014},
}

@book{Borceux:1994:1,
  title={Handbook of Categorical Algebra: Volume 1, Basic Category Theory},
  author={Borceux, F.},
  isbn={9780521441780},
  lccn={93003225},
  series={Cambridge Textbooks in Linguistics},
  url={https://books.google.com/books?id=YfzImoopB-IC},
  year={1994},
  publisher=cup
}

@book{Borceux:1994:2,
  title={Handbook of Categorical Algebra: Volume 2, Categories and Structures},
  author={Borceux, F.},
  isbn={9780521441797},
  lccn={93003225},
  series={Cambridge Studies in Philosophy},
  year={1994},
  publisher=cup
}

@inproceedings{Fiore:1994,
  author    = {Marcelo P. Fiore and
               Gordon D. Plotkin},
  title     = {An Axiomatization of Computationally Adequate Domain Theoretic Models
               of {FPC}},
  booktitle = lics94,
  pages     = {92--102},
  year      = {1994}
}

@article{Pitts:1996,
  title = "Relational Properties of Domains",
  journal = ic,
  volume = "127",
  number = "2",
  pages = "66--90",
  year = "1996",
  issn = "0890-5401",
  author = "Andrew M. Pitts",
  publisher = elsevier
}

@article{DBLP:journals/tcs/ArnoldN80,
  author    = {Andr{\'{e}} Arnold and
               Maurice Nivat},
  title     = {Metric Interpretations of Infinite Trees and Semantics of non-Deterministic
               Recursive Programs},
  journal   = tcs,
  volume    = {11},
  number    = {2},
  pages     = {181--205},
  year      = {1980},
  url       = {http://dx.doi.org/10.1016/0304-3975(80)90045-6},
  publisher = elsevier
}

@inproceedings{DBLP:conf/stoc/DeBakkerZ82,
  author    = {de Bakker, J. W. and
               Zucker, Jeffrey I.},
  title     = {Denotational Semantics of Concurrency},
  booktitle = stoc82,
  pages     = {153--158},
  year      = {1982},
  url       = {http://doi.acm.org/10.1145/800070.802188},
}

@inproceedings{DBLP:conf/mfps/AmericaR87,
  author    = {Pierre America and
               Jan J. M. M. Rutten},
  title     = {Solving Reflexive Domain Equations in a Category of Complete Metric
               Spaces},
  booktitle = mfps87,
  series    = lncs,
  publisher = springer,
  volume    = 298,
  pages     = {254--288},
  year      = {1987},
  url       = {http://dx.doi.org/10.1007/3-540-19020-1_13},
}

@article{Baier1994,
title = "Denotational semantics in the {CPO} and metric approach",
journal = tcs,
volume = "135",
number = "2",
pages = "171--220",
year = "1994",
issn = "0304-3975",
url = "http://dx.doi.org/10.1016/0304-3975(94)00046-8",
author = "Christel Baier and Mila E. Majster{-}Cederbaum",
publisher = elsevier,
}

@article{DBLP:journals/ipl/Majster-Cederbaum88,
  author    = {Mila E. Majster{-}Cederbaum},
  title     = {On the Uniqueness of Fixed Points of Endofunctors in a Category of
               Complete Metric Spaces},
  journal   = {Information Processing Letters},
  volume    = {29},
  number    = {6},
  pages     = {277--281},
  year      = {1988},
  url       = {http://dx.doi.org/10.1016/0020-0190(88)90224-4},
  publisher = elsevier
}

@article{DBLP:journals/iandc/CederbaumZ91,
  author    = {Mila E. Majster{-}Cederbaum and
               F. Zetzsche},
  title     = {Towards a Foundation for Semantics in Complete Metric Spaces},
  journal   = ic,
  volume    = {90},
  number    = {2},
  pages     = {217--243},
  year      = {1991},
  url       = {http://dx.doi.org/10.1016/0890-5401(91)90005-M},
  publisher = elsevier
}

@article{DBLP:journals/tcs/Majster-CederbaumZ94,
  author    = {Mila E. Majster{-}Cederbaum and
               F. Zetzsche},
  title     = {The Comparison of a {CPO}-based Semantics with a {CMS}-based semantics
               for {CSP}},
  journal   = tcs,
  volume    = {124},
  number    = {1},
  pages     = {1--40},
  year      = {1994},
  url       = {http://dx.doi.org/10.1016/0304-3975(94)90052-3},
  publisher = elsevier
}

@article{DBLP:journals/tcs/Breugel01,
  author    = {van Breugel, Franck},
  title     = {An introduction to metric semantics: operational and denotational
               models for programming and specification languages},
  journal   = tcs,
  volume    = {258},
  number    = {1--2},
  pages     = {1--98},
  year      = {2001},
  url       = {http://dx.doi.org/10.1016/S0304-3975(00)00403-5},
  publisher = elsevier
}

@MISC{Escardo98ametric,
  author = {Martín H\"otzel Escard\'o},
  title = {A metric model of {PCF}},
  note = {Workshop on Realizability Semantics and Applications, Trento, Italy},
  url  = {http://www.cs.bham.ac.uk/~mhe/papers/metricpcf.pdf},
  year = {1999}
}

@article{GSS92,
  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},
  publisher=elsevier
}


@article{DBLP:journals/tcs/Ehrhard12,
  author    = {Thomas Ehrhard},
  title     = {The Scott model of linear logic is the extensional collapse of its
               relational model},
  journal   = tcs,
  volume    = {424},
  pages     = {20--45},
  year      = {2012},
  url       = {http://dx.doi.org/10.1016/j.tcs.2011.11.027},
  doi       = {10.1016/j.tcs.2011.11.027},
  publisher = elsevier
}

@inproceedings{DBLP:conf/popl/MacQueenPS84,
  author    = {David B. MacQueen and
               Gordon D. Plotkin and
               Ravi Sethi},
  title     = {An Ideal Model for Recursive Polymorphic Types},
  booktitle = popl84,
  pages     = {165--174},
  year      = {1984},
  url       = {http://doi.acm.org/10.1145/800017.800528},
}

@inproceedings{DBLP:conf/lics/AbadiPP89,
  author    = {Mart{\'{\i}}n Abadi and
               Benjamin C. Pierce and
               Gordon D. Plotkin},
  title     = {Faithful Ideal Models for Recursive Polymorphic Types},
  booktitle = lics89,
  pages     = {216--225},
  year      = {1989},
  url       = {http://dx.doi.org/10.1109/LICS.1989.39176}
}

@article{DBLP:journals/iandc/Amadio91,
  author    = {Roberto M. Amadio},
  title     = {Recursion over Realizability Structures},
  journal   = ic,
  volume    = {91},
  number    = {1},
  pages     = {55--85},
  year      = {1991},
  url       = {http://dx.doi.org/10.1016/0890-5401(91)90074-C},
  doi       = {10.1016/0890-5401(91)90074-C},
  publisher = elsevier
}


@inproceedings{DBLP:conf/lics/AbadiP90,
  author    = {Mart{\'{\i}}n Abadi and
               Gordon D. Plotkin},
  title     = {A {PER} Model of Polymorphism and Recursive Types},
  booktitle = lics90,
  pages     = {355--365},
  year      = {1990},
  url       = {http://dx.doi.org/10.1109/LICS.1990.113761},
}

@inproceedings{DBLP:conf/tlca/Chroboczek01,
  author    = {Juliusz Chroboczek},
  title     = {Subtyping Recursive Games},
  booktitle = tlca01,
  series    = lncs,
  volume    = 2044,
  publisher = springer,
  pages     = {61--75},
  year      = {2001},
  url       = {http://dx.doi.org/10.1007/3-540-45413-6_9},
}

@article{DBLP:journals/tcs/BirkedalST10,
  author    = {Lars Birkedal and
               Kristian St{\o}vring and
               Jacob Thamsborg},
  title     = {The category-theoretic solution of recursive metric-space equations},
  journal   = tcs,
  volume    = {411},
  number    = {47},
  pages     = {4102--4122},
  year      = {2010},
  url       = {http://dx.doi.org/10.1016/j.tcs.2010.07.010},
  publisher = elsevier
}

@inproceedings{DBLP:conf/fossacs/BirkedalST09,
  author    = {Lars Birkedal and
               Kristian St{\o}vring and
               Jacob Thamsborg},
  title     = {Realizability Semantics of Parametric Polymorphism, General References,
               and Recursive Types},
  booktitle = fossacs09,
  pages     = {456--470},
  year      = {2009},
  series    = lncs,
  publisher = springer,
  volume    = 5504,
  url       = {http://dx.doi.org/10.1007/978-3-642-00596-1_32},
}

@inproceedings{DBLP:conf/fossacs/SchwinghammerBS11,
  author    = {Jan Schwinghammer and
               Lars Birkedal and
               Kristian St{\o}vring},
  title     = {A Step-Indexed {K}ripke Model of Hidden State via Recursive Properties
               on Recursively Defined Metric Spaces},
  booktitle =  fossacs11,
  pages     = {305--319},
  year      = {2011},
  series    = lncs,
  publisher = springer,
  volume    = 6604,
  url       = {http://dx.doi.org/10.1007/978-3-642-19805-2_21}
}

@inproceedings{DBLP:conf/lics/Nakano00,
  author    = {Hiroshi Nakano},
  title     = {A Modality for Recursion},
  booktitle = lics00,
  pages     = {255--266},
  year      = {2000},
  url       = {http://dx.doi.org/10.1109/LICS.2000.855774},
}

@inproceedings{DBLP:conf/lics/BirkedalMSS11,
  author    = {Lars Birkedal and
               Rasmus Ejlers M{\o}gelberg and
               Jan Schwinghammer and
               Kristian St{\o}vring},
  title     = {First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the
               Topos of Trees},
  booktitle = lics11,
  pages     = {55--64},
  year      = {2011},
  url       = {http://dx.doi.org/10.1109/LICS.2011.16},
}

@inproceedings{DBLP:conf/icfp/2011,
  editor    = {Manuel M. T. Chakravarty and
               Zhenjiang Hu and
               Olivier Danvy},
  title     = icfp11,
  year      = {2011},
  isbn      = {978-1-4503-0865-6},
}

@inproceedings{DBLP:conf/lics/KrishnaswamiB11,
  author    = {Neelakantan R. Krishnaswami and
               Nick Benton},
  title     = {Ultrametric Semantics of Reactive Programs},
  booktitle = lics11,
  pages     = {257--266},
  year      = {2011},
  url       = {http://dx.doi.org/10.1109/LICS.2011.38},
}

@article{csiszarS04,
url = {http://dx.doi.org/10.1561/0100000004},
year = {2004},
volume = {1},
journal = {Foundations and Trends® in Communications and Information Theory},
title = {Information Theory and Statistics: {A} Tutorial},
doi = {10.1561/0100000004},
issn = {1567-2190},
number = {4},
pages = {417--528},
author = {I. Csiszár and P. C. Shields},
publisher = now
}

@article{DBLP:journals/entcs/BaierK97,
  author    = {Christel Baier and
               Marta Z. Kwiatkowska},
  title     = {Domain equations for probabilistic processes},
  journal   = entcs,
  volume    = {7},
  pages     = {34--54},
  year      = {1997},
  url       = {http://dx.doi.org/10.1016/S1571-0661(05)80465-7},
  publisher = elsevier,
}

@article{DBLP:journals/entcs/HartogVB00,
  author    = {den Hartog, Jerry  and
               de Vink, Erik P. and
               de Bakker, J. W.},
  title     = {Metric Semantics and Full Abstractness for Action Refinement and Probabilistic
               Choice},
  journal   = entcs,
  volume    = {40},
  pages     = {72--99},
  year      = {2000},
  url       = {http://dx.doi.org/10.1016/S1571-0661(05)80038-6},
  publisher = elsevier,
}

@inproceedings{DBLP:conf/lics/DesharnaisJGP02,
  author    = {Josee Desharnais and
               Radha Jagadeesan and
               Vineet Gupta and
               Prakash Panangaden},
  title     = {The Metric Analogue of Weak Bisimulation for Probabilistic Processes},
  booktitle = lics02,
  pages     = {413--422},
  year      = {2002},
  url       = {http://dx.doi.org/10.1109/LICS.2002.1029849},
}

@Unpublished{PlotkinGD:lecppf,
  author =	"Gordon Plotkin",
  title =	"Lectures on Predomains and Partial Functions",
  year =        "1985",
  note =        "Notes for a course given at the Center for the Study
                 of Language and Information, Stanford",
}

@inproceedings{HaeberlenPN11,
  author    = {Andreas Haeberlen and
               Benjamin C. Pierce and
               Arjun Narayan},
  title     = {Differential Privacy Under Fire},
  booktitle = usenix11,
  year      = {2011},
  url       = {http://static.usenix.org/events/sec11/tech/full_papers/Haeberlen.pdf},
}

@incollection{Jonsson:2001,
	Address = {Amsterdam},
	Author = {Jonsson, Bengt and Yi, Wang and Larsen, Kim G.},
	Booktitle = {Handbook of Process Algebra},
	Pages = {685-710},
	Publisher = {Elsevier},
	Title = {Probabilistic Extensions of Process Algebras},
  url = {citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.7376},
	Year = {2001}}

@inproceedings{HoangR10,
  author    = {Hoang, Viet Tung and
               Rogaway, Phillip},
  title     = {On Generalized {F}eistel Networks},
  booktitle = crypto10,
  series    = {Lecture Notes in Computer Science},
  volume    = {6223},
  pages     = {613--630},
  publisher = springer,
  url       = {https://eprint.iacr.org/2010/301.pdf},
  year      = {2010}
}

@inproceedings{Mironov02,
  author    = {Ilya Mironov},
  title     = {({N}ot So) Random Shuffles of {RC4}},
  booktitle = crypto02,
  series    = {Lecture Notes in Computer Science},
  volume    = {2442},
  pages     = {304--319},
  publisher = springer,
  year      = {2002},
  url       = {https://eprint.iacr.org/2002/067.pdf}
}

@inproceedings{Barr70,
author={Michael Barr}, 
title={Relational algebras},
editor={Mac Lane, S.},
booktitle={Reports of the Midwest Category Seminar, {IV}},
series={Lecture Notes in Mathematics},
volume={137},
year={1970},
pages={39–55}, 
url={http://www.math.mcgill.ca/barr/papers/relalgs.pdf},
publisher=springer
}

@article{DBLP:journals/corr/ChenM15e,
  author    = {Yan Chen and
               Ashwin Machanavajjhala},
  title     = {On the Privacy Properties of Variants on the Sparse Vector Technique},
  journal   = {CoRR},
  volume    = {abs/1508.07306},
  year      = {2015},
  url       = {http://arxiv.org/abs/1508.07306},
  timestamp = {Tue, 01 Sep 2015 14:42:40 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/ChenM15e},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@book{royden-analysis,
  title={Real Analysis},
  author={Royden, Halsey L. and Fitzpatrick, Patrick},
  isbn={9780131437470},
  lccn={2009048692},
  year={2010},
  edition={Fourth},
  publisher=ph
}

@book{dijkstra1976discipline,
  title={A discipline of programming},
  author={Dijkstra, Edsger W.},
  series={Series in Automatic Computation},
  publisher=ph,
  year={1976}
}

@article{OHEARN2007271,
  title = "Resources, concurrency, and local reasoning",
  journal = tcs,
  volume = "375",
  number = "1",
  pages = "271--307",
  year = "2007",
  note = "Festschrift for John C. Reynolds's 70th birthday",
  issn = "0304-3975",
  doi = "http://dx.doi.org/10.1016/j.tcs.2006.12.035",
  author = "Peter W. O'Hearn",
  publisher=elsevier
}

@article{Jones:2003:EST:858595.858602,
 author = {Jones, Cliff B.},
 title = {The Early Search for Tractable Ways of Reasoning About Programs},
 journal = {Annals of the History of Computing},
 issue_date = {April 2003},
 volume = {25},
 number = {2},
 month = apr,
 year = {2003},
 issn = {1058-6180},
 pages = {26--49},
 numpages = {24},
 url = {https://pdfs.semanticscholar.org/edf2/372be96bc9c1f138e691bf0d222eafc64b55.pdf},
 doi = {10.1109/MAHC.2003.1203057},
 acmid = {858602},
 publisher = ieee,
 address = {Piscataway, NJ, USA},
} 

@article{Apt:1981:TYH:357146.357150,
  author = {Apt, Krzysztof R.},
  title = {Ten Years of {H}oare's Logic: {A} Survey--Part {I}},
  journal = toplas,
  issue_date = {Oct. 1981},
  volume = {3},
  number = {4},
  month = oct,
  year = {1981},
  issn = {0164-0925},
  pages = {431--483},
  numpages = {53},
  url = {http://doi.acm.org/10.1145/357146.357150},
  doi = {10.1145/357146.357150},
  acmid = {357150},
  publisher = {ACM},
  address = {New York, NY, USA},
}

@article{APT198383,
  title = "Ten years of {H}oare's logic: {A} survey--Part {II}: Nondeterminism",
  journal = tcs,
  volume = "28",
  number = "1",
  pages = "83--109",
  year = "1983",
  issn = "0304-3975",
  doi = "http://dx.doi.org/10.1016/0304-3975(83)90066-X",
  url = "http://www.sciencedirect.com/science/article/pii/030439758390066X",
  author = {Apt, Krzysztof R.},
  publisher=elsevier
}

@article{YANG2007308,
  title = "Relational separation logic",
  journal = tcs,
  volume = "375",
  number = "1",
  pages = "308--334",
  year = "2007",
  note = "Festschrift for John C. Reynolds's 70th birthday",
  issn = "0304-3975",
  doi = "http://dx.doi.org/10.1016/j.tcs.2006.12.036",
  url = "http://www.sciencedirect.com/science/article/pii/S0304397506009261",
  author = "Hongseok Yang",
  publisher=elsevier
}

@inproceedings{DBLP:conf/pst/EbadiAS16,
  author    = {Hamid Ebadi and
               Thibaud Antignac and
               David Sands},
  title     = {Sampling and partitioning for differential privacy},
  booktitle = {Conference on Privacy, Security and Trust ({PST}),
               Auckland, New Zealand},
  pages     = {664--673},
  year      = {2016},
  publisher = {{IEEE}},
  url       = {https://doi.org/10.1109/PST.2016.7906954},
}

@inproceedings{DBLP:conf/popl/EbadiSS15,
  author    = {Hamid Ebadi and
               David Sands and
               Gerardo Schneider},
  title     = {Differential Privacy: Now it's Getting Personal},
  booktitle = popl15,
  pages     = {69--81},
  year      = {2015},
  url       = {http://doi.acm.org/10.1145/2676726.2677005},
}

@article{ebadi2016featherweight,
  title={Featherweight {PINQ}},
  author={Ebadi, Hamid and Sands, David},
  journal=jpc,
  volume={7},
  number={2},
  pages={159--184},
  year={2016}
}

@inproceedings{proserpio2014calibrating,
  title={Calibrating data to sensitivity in private data analysis:
         {A} platform for differentially-private analysis of weighted datasets},
  author={Proserpio, Davide and Goldberg, Sharon and {McSherry}, Frank},
  booktitle=vldb14,
  volume={7},
  number={8},
  pages={637--648},
  year={2014},
}

@inproceedings{palamidessi:hal-00760688,
  TITLE = {Differential privacy for relational algebra: {Improving} the sensitivity bounds via constraint systems},
  AUTHOR = {Palamidessi, Catuscia and Stronati, Marco},
  URL = {https://hal.inria.fr/hal-00760688},
  BOOKTITLE = {Workshop on Quantitative Aspects of Programming
               Languages ({QAPL}), Tallin, Estonia},
  PUBLISHER = {Open Publishing Association},
  SERIES = eptcs,
  VOLUME = {85},
  PAGES = {92--105},
  YEAR = {2012},
  MONTH = Apr,
  DOI = {10.4204/EPTCS.85.7},
  PDF = {https://hal.inria.fr/hal-00760688/file/paper.pdf},
  HAL_ID = {hal-00760688},
  HAL_VERSION = {v1},
}

@mastersthesis{buch:thesis,
  title = {Formalizing Differential Privacy},
  author = {Buch, Mads},
  school = {Aarhus University},
  url = {http://madsbuch.com/thesis},
  year = 2017
}