6698 lines
200 KiB
BibTeX
6698 lines
200 KiB
BibTeX
%%%%%%%%%%%%%%%%%%%%%%%%%%%% UNPUBLISHED %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||
@unpublished{ABHS18,
|
||
title = {Almost Sure Productivity},
|
||
author = {Aguirre, Alejandro and
|
||
Barthe, Gilles and
|
||
Hsu, Justin and
|
||
Silva, Alexandra},
|
||
year = {2018},
|
||
jh = yes,
|
||
url = {https://justinh.su/files/docs/asp.pdf},
|
||
}
|
||
|
||
@unpublished{AH18,
|
||
title = {Constraint-Based Synthesis of Coupling Proofs},
|
||
author = {Albarghouthi, Aws and
|
||
Hsu, Justin},
|
||
year = {2018},
|
||
jh = yes,
|
||
}
|
||
|
||
@unpublished{SBGHK17,
|
||
title = {Reasoning about Divergences for Relaxations of Differential Privacy},
|
||
author = {Sato, Tetsuya and
|
||
Barthe, Gilles and
|
||
Gaboradi, Marco and
|
||
Hsu, Justin and
|
||
Katsumata, {Shin-ya}},
|
||
year = {2018},
|
||
url = {https://arxiv.org/abs/1710.09010},
|
||
jh = yes,
|
||
eprint = {1710.09010},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.PL},
|
||
}
|
||
|
||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% THESIS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||
|
||
@phdthesis{JHThesis,
|
||
title = {Probabilistic Couplings for Probabilistic Reasoning},
|
||
author = {Justin Hsu},
|
||
school = {University of Pennsylvania},
|
||
year = {2017},
|
||
url = {https://arxiv.org/abs/1710.09951},
|
||
jh = yes,
|
||
eprint = {1710.09951},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.LO}
|
||
}
|
||
|
||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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 = {https://arxiv.org/abs/1402.1526},
|
||
eprint = {1402.1526},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.DS},
|
||
publisher = bepress,
|
||
jh = yes,
|
||
reviewed = yes,
|
||
poster = {https://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 = {https://arxiv.org/abs/1311.2828},
|
||
eprint = {1311.2828},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.GT},
|
||
jh = yes,
|
||
reviewed = yes,
|
||
poster = {https://justinh.su/files/posters/matchings.pdf},
|
||
note = "Previously published in " # stoc14 # ", 2014."
|
||
}
|
||
|
||
%%%%%%%%%%%%%%%%%%%%%%%%%%%% CONFERENCES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||
@inproceedings{BEGGHS16,
|
||
title = {A Program Logic for Probabilistic Programs},
|
||
author = {Barthe, Gilles and
|
||
Espitau, Thomas and
|
||
Gaboardi, Marco and
|
||
Gr{\'e}goire, Benjamin and
|
||
Hsu, Justin and
|
||
Strub, {Pierre}-{Yves}},
|
||
year = {2018},
|
||
jh = yes,
|
||
reviewed = yes,
|
||
booktitle = esop18,
|
||
url = {https://justinh.su/files/papers/ellora.pdf},
|
||
note = "To appear.",
|
||
}
|
||
|
||
@article{AH17,
|
||
title = {Synthesizing Coupling Proofs of Differential Privacy},
|
||
author = {Albarghouthi, Aws and
|
||
Hsu, Justin},
|
||
year = {2018},
|
||
month = jan,
|
||
jh = yes,
|
||
journal = pacmpl,
|
||
volume = {2},
|
||
number = {POPL},
|
||
articleno = {58},
|
||
url = {https://arxiv.org/abs/1709.05361},
|
||
note = "Appeared at " # popl18 # ".",
|
||
reviewed = yes,
|
||
doi = {10.1145/3158146},
|
||
eprint = {1709.05361},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.PL},
|
||
}
|
||
|
||
@article{BEGHS16,
|
||
title = {Proving Expected Sensitivity of Probabilistic Programs},
|
||
author = {Barthe, Gilles and
|
||
Espitau, Thomas and
|
||
Gr{\'e}goire, Benjamin and
|
||
Hsu, Justin and
|
||
Strub, {Pierre}-{Yves}},
|
||
year = {2018},
|
||
month = jan,
|
||
jh = yes,
|
||
journal = pacmpl,
|
||
volume = {2},
|
||
number = {POPL},
|
||
articleno = {57},
|
||
doi = {10.1145/3158145},
|
||
url = {https://arxiv.org/abs/1708.02537},
|
||
note = "Appeared at " # popl18 # ".",
|
||
reviewed = yes,
|
||
slides = {https://justinh.su/files/slides/eprhl.pdf},
|
||
eprint = {1708.02537},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.PL},
|
||
}
|
||
|
||
@inproceedings{BEHSS17,
|
||
title = {$\star$-Liftings for Differential Privacy},
|
||
author = {Barthe, Gilles and
|
||
Espitau, Thomas and
|
||
Hsu, Justin and
|
||
Sato, Tetsuya and
|
||
Strub, {Pierre}-{Yves}},
|
||
booktitle = icalp17,
|
||
year = 2017,
|
||
pages ={102:1--102:12},
|
||
series = lipics,
|
||
volume = 80,
|
||
publisher = dagstuhl,
|
||
url = {https://arxiv.org/abs/1705.00133},
|
||
eprint = {1705.00133},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.LO},
|
||
doi = {10.4230/LIPIcs.ICALP.2017.102},
|
||
slides = {https://justinh.su/files/slides/star-lifting.pdf},
|
||
jh = yes,
|
||
plclub = yes,
|
||
reviewed = yes,
|
||
acceptance = {137/459=0.29},
|
||
}
|
||
|
||
@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, {Pierre}-{Yves}},
|
||
booktitle = lpar17,
|
||
pages = {385--403},
|
||
series = epic,
|
||
volume = 46,
|
||
year = 2017,
|
||
url = {https://arxiv.org/abs/1701.06477},
|
||
eprint = {1701.06477},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.PL},
|
||
slides = {https://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, {Pierre}-{Yves}},
|
||
booktitle = popl17,
|
||
pages = {161--174},
|
||
year = 2017,
|
||
url = {https://arxiv.org/abs/1607.03455},
|
||
eprint = {1607.03455},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.PL},
|
||
doi = {10.1145/3009837.3009896},
|
||
slides = {https://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 = {Azevedo de Amorim, Arthur and
|
||
Gaboardi, Marco and
|
||
Hsu, Justin and
|
||
Katsumata, {Shin-ya} and
|
||
Cherigui, Ikram},
|
||
booktitle = popl17,
|
||
year = 2017,
|
||
pages = {545--556},
|
||
url = {https://arxiv.org/abs/1702.00374},
|
||
eprint = {1702.00374},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.PL},
|
||
doi = {10.1145/3009837.3009890},
|
||
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 = {https://arxiv.org/abs/1502.04052},
|
||
eprint = {1502.04052},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.GT},
|
||
doi = {10.1007/978-3-662-54110-4_20},
|
||
slides = {https://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, {Pierre}-{Yves}},
|
||
booktitle = ccs16,
|
||
year = 2016,
|
||
pages = {55--67},
|
||
url = {https://arxiv.org/abs/1606.07143},
|
||
eprint = {1606.07143},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.LO},
|
||
doi = {10.1145/2976749.2978391},
|
||
jh = yes,
|
||
plclub = yes,
|
||
reviewed = yes,
|
||
slides = {https://justinh.su/files/slides/advanced.pdf},
|
||
acceptance = {137/831=0.17},
|
||
note = {There is an error in the treatment of advanced composition;
|
||
please see my thesis for the correction.},
|
||
}
|
||
|
||
@inproceedings{privinfer,
|
||
title = {Differentially Private {Bayesian} 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},
|
||
eprint = {1605.00283},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.PL},
|
||
doi = {10.1145/2976749.2978371},
|
||
jh = yes,
|
||
plclub = yes,
|
||
reviewed = yes,
|
||
acceptance = {137/831=0.17},
|
||
}
|
||
|
||
@inproceedings{BEFFH16,
|
||
title = {Synthesizing Probabilistic Invariants via {Doob}'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},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.PL},
|
||
eprint = {1605.02765},
|
||
doi = {10.1007/978-3-319-41528-4_3},
|
||
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, {Pierre}-{Yves}},
|
||
booktitle = icalp16,
|
||
pages = {107:1--107:15},
|
||
volume = {55},
|
||
series = lipics,
|
||
year = 2016,
|
||
publisher = dagstuhl,
|
||
url = {https://arxiv.org/abs/1602.05681},
|
||
eprint = {1602.05681},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.LO},
|
||
doi = {10.4230/LIPIcs.ICALP.2016.107},
|
||
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, {Pierre}-{Yves}},
|
||
booktitle = lics16,
|
||
pages = {749--758},
|
||
year = 2016,
|
||
url = {https://arxiv.org/abs/1601.05047},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.LO},
|
||
eprint = {1601.05047},
|
||
doi = {10.1145/2933575.2934554},
|
||
jh = yes,
|
||
plclub = yes,
|
||
reviewed = yes,
|
||
slides = {https://justinh.su/files/slides/approx-couplings.pdf},
|
||
acceptance = {85/191=0.44}
|
||
}
|
||
|
||
@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 = {https://arxiv.org/abs/1511.00925},
|
||
eprint = {1511.00925},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.GT},
|
||
doi = {10.1145/2897518.2897559},
|
||
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 = {https://arxiv.org/abs/1411.0998},
|
||
eprint = {1411.0998},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.DS},
|
||
doi = {10.1137/1.9781611974331.ch43},
|
||
jh = yes,
|
||
reviewed = yes,
|
||
slides = {https://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, {Pierre}-{Yves}},
|
||
booktitle = lpar15,
|
||
pages = {387--401},
|
||
volume = {9450},
|
||
series = lncs,
|
||
year = 2015,
|
||
publisher = springer,
|
||
url = {https://arxiv.org/abs/1509.03476},
|
||
eprint = {1509.03476},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.LO},
|
||
doi = {10.1007/978-3-662-48899-7_27},
|
||
jh = yes,
|
||
plclub = yes,
|
||
reviewed = yes,
|
||
slides = {https://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 = {https://arxiv.org/abs/1508.03593},
|
||
eprint = {1508.03593},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.DS},
|
||
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 = {https://justinh.su/files/papers/theory-ab.pdf},
|
||
doi = {10.4230/LIPIcs.SNAPL.2015.129},
|
||
jh = yes,
|
||
plclub = yes,
|
||
reviewed = yes,
|
||
slides = {https://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 = {https://arxiv.org/abs/1407.6845},
|
||
eprint = {1407.6845},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.PL},
|
||
doi = {10.1145/2676726.2677000},
|
||
jh = yes,
|
||
plclub = yes,
|
||
reviewed = yes,
|
||
slides = {https://justinh.su/files/slides/hoare2.pdf},
|
||
acceptance = {52/227=0.23},
|
||
}
|
||
|
||
@inproceedings{AGGH14,
|
||
author = {Azevedo de Amorim, Arthur 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 = {https://arxiv.org/abs/1503.04522},
|
||
eprint = {1503.04522},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.LO},
|
||
doi = {10.1145/2746325.2746335},
|
||
jh = yes,
|
||
plclub = yes,
|
||
reviewed = yes,
|
||
slides = {https://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 {Hoare} Logic},
|
||
booktitle = csf14,
|
||
pages = {411--424},
|
||
year = {2014},
|
||
url = {https://arxiv.org/abs/1407.2988},
|
||
eprint = {1407.2988},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.LO},
|
||
doi = {10.1109/CSF.2014.36},
|
||
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 = {https://arxiv.org/abs/1402.3329},
|
||
eprint = {1402.3329},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.DB},
|
||
doi = {10.1109/CSF.2014.35},
|
||
jh = yes,
|
||
plclub = yes,
|
||
reviewed = yes,
|
||
slides = {https://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 = {https://arxiv.org/abs/1402.3631},
|
||
eprint = {1402.3631},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.DS},
|
||
doi = {10.1007/978-3-662-43948-7_51},
|
||
jh = yes,
|
||
reviewed = yes,
|
||
slides = {https://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 = pmlr,
|
||
year = {2014},
|
||
reviewed = yes,
|
||
url = {https://arxiv.org/abs/1402.1526},
|
||
eprint = {1402.1526},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.DS},
|
||
jh = yes,
|
||
slides = {https://justinh.su/files/slides/dualquery.pdf},
|
||
poster = {https://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 = {https://arxiv.org/abs/1311.2828},
|
||
eprint = {1311.2828},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.GT},
|
||
doi = {10.1145/2591796.2591826},
|
||
timestamp = {Wed, 22 Oct 2014 14:44:14 +0200},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/conf/stoc/HsuHRRW14},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org},
|
||
jh = yes,
|
||
poster = {https://justinh.su/files/poster/matchings.pdf},
|
||
acceptance = {91/319=0.29},
|
||
}
|
||
|
||
@inproceedings{WHE13,
|
||
title = {{System} {FC} with Explicit Kind Equality},
|
||
author = {Weirich, Stephanie and
|
||
Hsu, Justin and
|
||
Eisenberg, Richard A.},
|
||
booktitle = icfp13,
|
||
pages = {275--286},
|
||
year = {2013},
|
||
url = {https://justinh.su/files/papers/nokinds.pdf},
|
||
doi = {10.1145/2500365.2500599},
|
||
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},
|
||
booktitle = stoc13,
|
||
pages = {341--350},
|
||
year = {2013},
|
||
url = {https://arxiv.org/abs/1211.0877},
|
||
eprint = {1211.0877},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.DS},
|
||
doi = {10.1145/2488608.2488651},
|
||
jh = yes,
|
||
reviewed = yes,
|
||
slides = {https://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 = {https://dl.acm.org/citation.cfm?id=2429113},
|
||
doi = {10.1145/2429069.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 = {https://arxiv.org/abs/1202.4910},
|
||
eprint = {1202.4910},
|
||
archivePrefix = {arXiv},
|
||
primaryClass = {cs.DS},
|
||
doi = {10.1007/978-3-642-31594-7_39},
|
||
note = {Thanks to Raef Bassily and Adam Smith for spotting an error, now fixed.},
|
||
jh = yes,
|
||
reviewed = yes,
|
||
slides = {https://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 = {https://siglog.hosting.acm.org/wp-content/uploads/2016/01/siglog_news_7.pdf},
|
||
doi = {10.1145/2893582.2893591},
|
||
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 = {https://justinh.su/files/slides/taxes.pdf},
|
||
url = {https://justinh.su/files/papers/taxes.pdf}
|
||
}
|
||
|
||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% TALKS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||
@talk{icalp17-talk,
|
||
title = {$\star$-Liftings for Differential Privacy},
|
||
organization = icalp17,
|
||
year = 2017,
|
||
month = jul,
|
||
jh = yes,
|
||
}
|
||
|
||
@talk{lpar17-talk,
|
||
title = {Proving Uniformity and Independence by Self-Composition and Coupling},
|
||
organization = lpar17,
|
||
year = 2017,
|
||
month = may,
|
||
jh = yes,
|
||
}
|
||
|
||
@talk{nw17-talk,
|
||
title = {Randomized Algorithms Meet Formal Verification},
|
||
organization = {Northwestern University},
|
||
year = 2017,
|
||
month = apr,
|
||
jh = yes,
|
||
}
|
||
|
||
@talk{mit17-talk,
|
||
title = {Randomized Algorithms Meet Formal Verification},
|
||
organization = {Massachusetts Institute of Technology},
|
||
year = 2017,
|
||
month = apr,
|
||
jh = yes,
|
||
}
|
||
|
||
@talk{cmu17-talk,
|
||
title = {Randomized Algorithms Meet Formal Verification},
|
||
organization = {Carnegie Mellon University},
|
||
year = 2017,
|
||
month = mar,
|
||
jh = yes,
|
||
}
|
||
|
||
@talk{dagstuhl17-talk,
|
||
title = {Differential Privacy and Incentive Properties},
|
||
organization = {Dagstuhl Seminar: Game Theory in {AI}, Logic, and Algorithms},
|
||
year = 2017,
|
||
month = mar,
|
||
jh = yes,
|
||
}
|
||
|
||
@talk{mpi17-talk,
|
||
title = {Randomized Algorithms Meet Formal Verification},
|
||
organization = {Max Planck Institute for Software Systems},
|
||
year = 2017,
|
||
month = mar,
|
||
jh = yes,
|
||
}
|
||
|
||
@talk{eth17-talk,
|
||
title = {Randomized Algorithms Meet Formal Verification},
|
||
organization = {{ETH} Z\"urich},
|
||
year = 2017,
|
||
month = mar,
|
||
jh = yes,
|
||
}
|
||
|
||
@talk{yale17-talk,
|
||
title = {Randomized Algorithms Meet Formal Verification},
|
||
organization = {Yale University},
|
||
year = 2017,
|
||
month = feb,
|
||
jh = yes,
|
||
}
|
||
|
||
@talk{nyu17-talk,
|
||
title = {Randomized Algorithms Meet Formal Verification},
|
||
organization = {Courant Institute, New York University},
|
||
year = 2017,
|
||
month = feb,
|
||
jh = yes,
|
||
}
|
||
|
||
@talk{wisc17-talk,
|
||
title = {Randomized Algorithms Meet Formal Verification},
|
||
organization = {University of Wisconsin--Madison},
|
||
year = 2017,
|
||
month = feb,
|
||
jh = yes,
|
||
}
|
||
|
||
@talk{ist17-talk,
|
||
title = {Randomized Algorithms Meet Formal Verification},
|
||
organization = {Institute of Science and Technology Austria},
|
||
year = 2017,
|
||
month = jan,
|
||
jh = yes,
|
||
}
|
||
|
||
@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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://arxiv.org/abs/1306.2083},
|
||
journal = sigecom,
|
||
year = {2013}
|
||
}
|
||
|
||
@inproceedings{NRS07,
|
||
title = {Smooth sensitivity and sampling in private data analysis},
|
||
url = {https://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 = {https://arxiv.org/abs/1311.2625}
|
||
}
|
||
|
||
@inproceedings{GLMRT10,
|
||
title = {Differentially private combinatorial optimization},
|
||
url = {https://arxiv.org/abs/0903.4510},
|
||
author = {Gupta, Anupam and Ligett, Katrina and {McSherry}, 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 = {https://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 = {https://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 = {https://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 = {https://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},
|
||
doi = {10.1561/0400000042},
|
||
url = {https://dx.doi.org/10.1561/0400000042},
|
||
timestamp = {Tue, 28 Oct 2014 14:00:24 +0100},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/journals/fttcs/DworkR14},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
@inproceedings{KPRU14,
|
||
title = {Mechanism Design in Large Games: Incentives and Privacy},
|
||
url = {https://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 = {https://research.microsoft.com/pubs/155170/dworkrv10.pdf},
|
||
booktitle = focs10,
|
||
author = {Dwork, Cynthia and Rothblum, Guy N. and Vadhan, Salil},
|
||
year = {2010},
|
||
doi = {10.1109/FOCS.2010.12},
|
||
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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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},
|
||
doi = {10.1109/FOCS.2007.66},
|
||
url = {https://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 = {https://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 {McSherry} and
|
||
Kobbi Nissim},
|
||
booktitle = pods05,
|
||
pages = {128--138},
|
||
url = {https://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 = {https://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 = {https://dl.acm.org/citation.cfm?id=1855731 },
|
||
year = 2010
|
||
}
|
||
|
||
@inproceedings{pinq,
|
||
author = {{McSherry}, Frank},
|
||
booktitle = sigmod09,
|
||
title = {Privacy Integrated Queries},
|
||
pages = {19--30},
|
||
url = {https://research.microsoft.com/pubs/80218/sigmod115-mcsherry.pdf},
|
||
doi = {10.1145/1559845.1559850},
|
||
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 = {https://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 = {https://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$-{Closeness}: {Privacy} 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 = {https://dl.acm.org/citation.cfm?id=774552}
|
||
}
|
||
|
||
@article{aol,
|
||
author = {Michael Barbaro and Tom Zeller},
|
||
title = {A Face Is Exposed for {AOL} Searcher {No.} 4417749},
|
||
journal = {The New York Times},
|
||
day = 9,
|
||
month = aug,
|
||
year = 2006,
|
||
url = {https://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 = {https://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 = {https://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 = {https://books.nips.cc/papers/files/nips21/NIPS2008_0964.pdf}
|
||
}
|
||
|
||
@inproceedings{CH11,
|
||
title = {Sample Complexity Bounds for Differentially Private Learning},
|
||
author = {Chaudhuri, Kamalika and Hsu, Daniel},
|
||
booktitle = colt11,
|
||
series = pmlr,
|
||
volume = {19},
|
||
pages = {155--186},
|
||
url = {https://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},
|
||
doi = {10.1145/2492061},
|
||
url = {https://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},
|
||
doi = {10.1145/1863543.1863568},
|
||
url = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://tocbeta.cs.uchicago.edu/articles/v008a006/v008a006.pdf},
|
||
year = {2012}
|
||
}
|
||
|
||
@phdthesis{Garg13,
|
||
title = {Candidate Multilinear Maps},
|
||
author = {Sanjam Garg},
|
||
school = {{UCLA}},
|
||
year = {2013},
|
||
url = {https://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 = {https://https://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 = {https://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 {McSherry}, Frank and Talwar, Kunal},
|
||
booktitle = pods07,
|
||
pages = {273--282},
|
||
url = {https://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 = {https://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 = {https://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 = {https://repository.cmu.edu/cgi/viewcontent.cgi?article=1065&context=jpc}
|
||
}
|
||
|
||
@inproceedings{KST12,
|
||
title = {Private convex empirical risk minimization and high-dimensional regression},
|
||
author = {Kifer, Daniel and Smith, Adam and Thakurta, Abhradeep},
|
||
booktitle = colt12,
|
||
series = pmlr,
|
||
volume = {23},
|
||
pages = {25.1--25.40},
|
||
year = {2012},
|
||
url = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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,
|
||
series = pmlr,
|
||
volume = 30,
|
||
pages = {819--850},
|
||
url = {https://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 = {https://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 = {https://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 = {https://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 {McGregor}, Andrew},
|
||
booktitle = pods10,
|
||
pages = {123--134},
|
||
year = {2010},
|
||
url = {https://arxiv.org/abs/0912.4742}
|
||
}
|
||
|
||
@article{LM12,
|
||
title = {An adaptive mechanism for accurate query answering under differential privacy},
|
||
author = {Li, Chao and Miklau, Gerome},
|
||
journal = pvldb,
|
||
note = vldb12,
|
||
volume = {5},
|
||
number = {6},
|
||
pages = {514--525},
|
||
year = {2012},
|
||
url = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://www.cs.cmu.edu/~joshuad/papers/tridirectional-typechecking/Dunfield04_tridirectional.pdf}
|
||
}
|
||
|
||
|
||
@article{Meyer92,
|
||
title = {Applying ``{Design} by contract''},
|
||
author = {Meyer, Bertrand},
|
||
journal = {Computer},
|
||
volume = {25},
|
||
number = {10},
|
||
pages = {40--51},
|
||
year = {1992},
|
||
publisher = {IEEE},
|
||
url = {https://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. {Peyton}-{Jones}},
|
||
title = {{Refinement Types for Haskell}},
|
||
booktitle = icfp14,
|
||
year = {2014},
|
||
url = {https://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 = {https://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, {Maria}-{Florina} 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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 {McIver}, Annabelle and Morgan, Carroll},
|
||
Journal = tcs,
|
||
Number = {1},
|
||
Pages = {96--112},
|
||
Title = {Probabilistic guarded commands mechanized in {HOL}},
|
||
Volume = {346},
|
||
Year = {2005},
|
||
url = {https://www.cse.unsw.edu.au/~carrollm/probs/Papers/Hurd-05.pdf}
|
||
}
|
||
|
||
@book{McIver:2005,
|
||
Author = {{McIver}, 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 = {https://cis.upenn.edu/~mgree/papers/esop2011_mts.pdf}
|
||
}
|
||
|
||
@inproceedings{Kiselyov:2009,
|
||
author = {Oleg Kiselyov and
|
||
{Chung}-{Chieh} 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 {McKinley}, Kathryn S and Grossman, Dan and Ceze, Luis},
|
||
booktitle = pldi14,
|
||
pages = {14},
|
||
year = {2014},
|
||
url = {https://research.microsoft.com/pubs/211410/passert-pldi2014.pdf}
|
||
}
|
||
|
||
@Inproceedings {Bornholt+14,
|
||
author = {James Bornholt and Todd Mytkowicz and Kathryn S {McKinley}},
|
||
booktitle = asplos14,
|
||
title = {{Uncertain$\langle$T$\rangle$}: {A} First-Order Type for Uncertain Data},
|
||
year = {2014},
|
||
url = {https://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 = {https://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, {Pierre}-{Yves} and Bhargavan, Karthikeyan and Yang, Jean},
|
||
title = {Secure distributed programming with value-dependent types},
|
||
booktitle = icfp11,
|
||
year = 2011,
|
||
url = {https://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 = {https://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, {Pierre}-{Yves} and
|
||
Swamy, Nikhil and
|
||
Zanella{-}B{\'e}guelin, Santiago},
|
||
booktitle = popl14,
|
||
pages = {193--206},
|
||
year = {2014},
|
||
doi = {10.1145/2535838.2535847},
|
||
url = {https://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 = {https://arxiv.org/abs/1406.2060}
|
||
}
|
||
|
||
|
||
@inproceedings{Dwork06,
|
||
Author = {Dwork, Cynthia},
|
||
Booktitle = icalp06,
|
||
Pages = {1--12},
|
||
Title = {Differential Privacy},
|
||
Year = {2006},
|
||
url = {https://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},
|
||
doi = {10.1145/964001.964003},
|
||
url = {https://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 = {https://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},
|
||
doi = {10.1145/1480881.1480894},
|
||
url = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://dx.doi.org/10.1016/j.ipl.2005.09.010},
|
||
bibsource = {DBLP, https://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 = {https://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 = {https://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 = {https://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 = {https://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,
|
||
doi = {10.1017/S0960129511000193},
|
||
url = {https://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},
|
||
doi = {10.1007/978-3-540-68237-0_5},
|
||
url = {https://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},
|
||
doi = {10.1007/11547662_24},
|
||
url = {https://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 = {https://software.imdea.org/~ckunz/rellog/long-rellog.pdf},
|
||
doi = {10.1007/978-3-642-21437-0_17}
|
||
}
|
||
|
||
@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,
|
||
doi = {10.1007/978--3-642--35722--0_3},
|
||
url = {https://dx.doi.org/10.1007/978--3-642--35722--0_3},
|
||
bibsource = {DBLP, https://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 = {https://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 = {https://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 = {https://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 =
|
||
{https://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 = {https://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 = {https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf}
|
||
}
|
||
|
||
@incollection{epigram,
|
||
title = {Epigram: Practical programming with dependent types},
|
||
author = {{McBride}, Conor},
|
||
booktitle = {Advanced Functional Programming},
|
||
pages = {130--170},
|
||
year = {2005},
|
||
publisher = springer,
|
||
url = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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},
|
||
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 = {https://arxiv.org/pdf/1101.2819v1},
|
||
doi = {10.1016/j.entcs.2011.09.015},
|
||
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 = {https://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 = {https://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 = {https://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 = {https://arxiv.org/abs/1407.7740},
|
||
timestamp = {Sun, 26 Oct 2014 15:36:31 +0100},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/journals/corr/CummingsKRW14},
|
||
bibsource = {dblp computer science bibliography, https://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 = {https://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 = {https://www.aaai.org/Library/ICML/2003/icml03-120.php},
|
||
timestamp = {Thu, 16 Oct 2014 21:45:09 +0200},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/conf/icml/Zinkevich03},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@article{JKT11,
|
||
title = {Differentially private online learning},
|
||
author = {Jain, Prateek and Kothari, Pravesh and Thakurta, Abhradeep Guha},
|
||
eprint = {1109.0105},
|
||
year = {2011},
|
||
url = {https://arxiv.org/abs/1109.0105}
|
||
}
|
||
|
||
@inproceedings{JT14,
|
||
title = {({Near}) Dimension Independent Risk Bounds for Differentially Private Learning},
|
||
author = {Jain, Prateek and Thakurta, Abhradeep Guha},
|
||
booktitle = icml14,
|
||
series = pmlr,
|
||
volume = 32,
|
||
pages = {476--484},
|
||
year = {2014},
|
||
url = {https://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 = {https://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 = {https://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 = {https://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 = {https://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,
|
||
doi = {10.1007/3-540-44802-0_1},
|
||
url = {https://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 = {https://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 = {https://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 = {https://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},
|
||
doi = {10.1109/LICS.2002.1029817},
|
||
url = {https://www.cs.cmu.edu/~jcr/seplogic.pdf}
|
||
}
|
||
|
||
@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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://software.imdea.org/~szanella/Zanella.2011.CRYPTO.pdf},
|
||
bibsource = {DBLP, https://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},
|
||
doi = {10.1007/978-3-319-10082-1_6},
|
||
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},
|
||
doi={10.1145/363235.363259},
|
||
url={https://dl.acm.org/citation.cfm?id=363259}
|
||
}
|
||
|
||
@incollection{Floyd67,
|
||
author = {Floyd, Robert W.},
|
||
booktitle = {Symposium on Applied Mathematics},
|
||
publisher = {American Mathematical Society},
|
||
title = {Assigning Meanings to Programs},
|
||
year = {1967},
|
||
doi = {10.1007/978-94-011-1793-7_4},
|
||
url = {https://link.springer.com/chapter/10.1007%2F978-94-011-1793-7_4}
|
||
}
|
||
|
||
|
||
@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 = "https://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},
|
||
doi = {10.1145/229542.229547},
|
||
url = {dl.acm.org/ft_gateway.cfm?id=229547}
|
||
}
|
||
|
||
@article{Kozen:1985,
|
||
author = {Dexter Kozen},
|
||
title = {A Probabilistic {PDL}},
|
||
journal = jcss,
|
||
volume = {30},
|
||
number = {2},
|
||
year = {1985},
|
||
doi = {10.1016/0022-0000(85)90012-1},
|
||
}
|
||
|
||
@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},
|
||
doi = {10.4204/EPTCS.147.9},
|
||
url = {https://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 = {https://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 = {https://dx.doi.org/10.1016/j.ipl.2005.09.010},
|
||
bibsource = {DBLP, https://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 = "https://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'Connor} and
|
||
Sidi Ould Biha and
|
||
Ioana Pasca and
|
||
Laurence Rideau and
|
||
Alexey Solovyev and
|
||
Enrico Tassi and
|
||
Laurent Th{\'{e}}ry},
|
||
title = {A Machine-Checked Proof of the Odd Order Theorem},
|
||
booktitle = {Interactive Theorem Proving (ITP)},
|
||
pages = {163--179},
|
||
year = {2013},
|
||
}
|
||
|
||
@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},
|
||
doi = {10.1007/11761679_25},
|
||
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}
|
||
}
|
||
|
||
@unpublished{Naumann:2009,
|
||
author = {Naumann, David A},
|
||
title = {Theory for software verification},
|
||
year = {2009},
|
||
url = {https://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 = "https://doi.acm.org/10.1145/1086365.1086375",
|
||
}
|
||
|
||
@article{McBrideMcKinna02,
|
||
author = {Conor {McBride} and James {McKinna}},
|
||
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 = {https://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 = "https://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 = {https://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 {Hoare} like logic},
|
||
author = {den Hartog, J I and de Vink, Erik P},
|
||
journal = {International Journal of Foundations of Computer Science},
|
||
volume = {13},
|
||
number = {03},
|
||
pages = {315--340},
|
||
year = {2002},
|
||
publisher = {World Scientific}
|
||
}
|
||
|
||
@article{Chadha07,
|
||
title = {Reasoning about probabilistic sequential programs},
|
||
author = {Chadha, Rohit and Cruz-Filipe, Lu{\'\i}s and Mateus, Paulo and
|
||
Sernadas, Am{\'\i}lcar},
|
||
journal = tcs,
|
||
volume = {379},
|
||
number = {1},
|
||
pages = {142--165},
|
||
year = {2007},
|
||
publisher = elsevier
|
||
}
|
||
|
||
@InProceedings{RandZ15,
|
||
author = {Robert Rand and Steve Zdancewic},
|
||
title = {{VPHL}: A Verified Partial-Correctness Logic for Probabilistic Programs},
|
||
booktitle = mfps15,
|
||
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 = jcss,
|
||
volume = {22},
|
||
number = {3},
|
||
pages = {328--350},
|
||
year = {1981},
|
||
publisher = {Elsevier},
|
||
doi = {10.1016/0022-0000(81)90036-2},
|
||
url = {https://www.sciencedirect.com/science/article/pii/0022000081900362}
|
||
}
|
||
|
||
@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},
|
||
doi = {10.1145/2676726.2677001}
|
||
}
|
||
|
||
@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 = {https://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 = {https://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={https://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={https://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={https://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={https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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={https://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={https://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 = {https://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 = {https://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 = {https://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={https://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 = {https://arxiv.org/abs/0808.1671},
|
||
}
|
||
|
||
@article{GS99a,
|
||
title = "The {English} Auction with Differentiated Commodities",
|
||
journal = jet,
|
||
volume = "92",
|
||
number = "1",
|
||
pages = "66--95",
|
||
year = "2000",
|
||
issn = "0022-0531",
|
||
url = "https://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 {Steinitz}'s exchange property},
|
||
url={https://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}-{Convex} Function on Generalized Polymatroid},
|
||
journal = {Mathematics of Operations Research},
|
||
volume = {24},
|
||
number = {1},
|
||
pages = {95--105},
|
||
year = {1999},
|
||
doi = {10.1287/moor.24.1.95},
|
||
}
|
||
|
||
@article{FY03,
|
||
author = {Fujishige, Satoru and Yang, Zaifu},
|
||
title = {A Note on {Kelso} and {Crawford}'s {Gross} {Substitutes} Condition},
|
||
journal = {Mathematics of Operations Research},
|
||
volume = {28},
|
||
number = {3},
|
||
pages = {463--469},
|
||
year = {2003},
|
||
doi = {10.1287/moor.28.3.463.16393},
|
||
}
|
||
|
||
@article{MT10,
|
||
title = "Characterization of the {Walrasian} equilibria of the assignment model ",
|
||
journal = "Journal of Mathematical Economics",
|
||
volume = "46",
|
||
number = "1",
|
||
pages = "6--20",
|
||
year = "2010",
|
||
issn = "0304-4068",
|
||
url = "https://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 = {https://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={https://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={https://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 = {https://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={https://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={https://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={https://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={https://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={https://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={https://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 = {https://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 = {https://arxiv.org/abs/1507.00473},
|
||
timestamp = {Sun, 02 Aug 2015 18:42:02 +0200},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/journals/corr/Hanneke15},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@book{pollard1984,
|
||
title= "Convergence of stochastic processes",
|
||
author={Pollard, David},
|
||
year={1984},
|
||
publisher={David Pollard},
|
||
url = {https://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={https://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={https://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},
|
||
doi = {10.1007/978-3-642-39212-2_8},
|
||
url = {https://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 = {https://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 = {https://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
|
||
}
|
||
|
||
@article{lyu2016understanding,
|
||
title={Understanding the {Sparse Vector Technique} for Differential Privacy},
|
||
author={Lyu, Min and Su, Dong and Li, Ninghui},
|
||
journal=pvldb,
|
||
note=vldb17,
|
||
volume=10,
|
||
number=6,
|
||
pages={637--648},
|
||
url={https://arxiv.org/abs/1603.01699},
|
||
doi={10.14778/3055330.3055331},
|
||
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},
|
||
}
|
||
|
||
@article{DBLP:journals/corr/OhV13,
|
||
author={P. Kairouz and S. Oh and P. Viswanath},
|
||
journal={IEEE Transactions on Information Theory},
|
||
title={The Composition Theorem for Differential Privacy},
|
||
year={2017},
|
||
volume={63},
|
||
number={6},
|
||
pages={4037--4049},
|
||
keywords={data privacy;composition theorem;data processing
|
||
inequality;differential privacy;privatization mechanisms;Data
|
||
privacy;Data processing;Databases;Electronic
|
||
mail;Privacy;Privatization;Testing;Differential privacy;hypothesis
|
||
testing},
|
||
doi={10.1109/TIT.2017.2685505},
|
||
url={https://arxiv.org/abs/1311.0776},
|
||
ISSN={0018-9448},
|
||
month={June},}
|
||
|
||
@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 {Markov} Chains},
|
||
author={Bubley, Russ and Dyer, Martin},
|
||
booktitle=focs97,
|
||
pages={223--231},
|
||
year={1997},
|
||
doi={10.1109/SFCS.1997.646111},
|
||
url={https://ieeexplore.ieee.org/document/646111/}
|
||
}
|
||
|
||
@unpublished{DworkRothblumCDP,
|
||
author = {Cynthia Dwork and
|
||
Guy N. Rothblum},
|
||
title = {Concentrated Differential Privacy},
|
||
journal = {CoRR},
|
||
volume = {abs/1603.01887},
|
||
year = {2016},
|
||
url = {https://arxiv.org/abs/1603.01887},
|
||
timestamp = {Wed, 07 Jun 2017 14:40:05 +0200},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/journals/corr/DworkR16},
|
||
bibsource = {dblp computer science bibliography, https://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},
|
||
volume = {9985},
|
||
doi = {10.1007/978-3-662-53641-4_24},
|
||
publisher = springer,
|
||
}
|
||
|
||
@inproceedings{MironovRDP,
|
||
title = {R\'enyi Differential Privacy},
|
||
author = {Ilya Mironov},
|
||
year = 2017,
|
||
URL = {https://arxiv.org/abs/1702.07476},
|
||
booktitle = csf17,
|
||
doi = {10.1109/CSF.2017.11},
|
||
pages = {263--275}
|
||
}
|
||
|
||
@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,
|
||
doi = {10.1137/1.9781611974782.85},
|
||
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},
|
||
doi={10.1109/LICS.1991.151651},
|
||
url={https://ieeexplore.ieee.org/document/151651/}
|
||
}
|
||
|
||
@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={https://arxiv.org/abs/1605.08294}
|
||
}
|
||
|
||
@inproceedings{sousa2016cartesian,
|
||
title={Cartesian {Hoare} Logic for Verifying $k$-Safety Properties},
|
||
author={Sousa, Marcelo and Dillig, Isil},
|
||
booktitle=pldi16,
|
||
pages={57--69},
|
||
year={2016},
|
||
doi={10.1145/2908080.2908092},
|
||
url={https://dl.acm.org/citation.cfm?id=2908092}
|
||
}
|
||
|
||
@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},
|
||
doi = {10.1145/3009837.3009884},
|
||
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 = {https://dx.doi.org/10.1137/0218077},
|
||
doi = {10.1137/0218077},
|
||
timestamp = {Mon, 12 Sep 2011 16:10:07 +0200},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/journals/siamcomp/JerrumS89},
|
||
bibsource = {dblp computer science bibliography, https://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 = {https://dx.doi.org/10.1002/rsa.3240070205},
|
||
doi = {10.1002/rsa.3240070205},
|
||
publisher = {Wiley},
|
||
timestamp = {Sat, 14 Apr 2012 16:35:21 +0200},
|
||
biburl =
|
||
{https://dblp.uni-trier.de/rec/bib/journals/rsa/Jerrum95},
|
||
bibsource = {dblp computer science bibliography,
|
||
https://dblp.org}
|
||
}
|
||
|
||
@inproceedings{Sato16,
|
||
title = {Approximate Relational {Hoare} Logic for Continuous Random Samplings},
|
||
author = {Tetsuya Sato},
|
||
booktitle = mfps16,
|
||
pages = {277--298},
|
||
year = 2016,
|
||
volume = 325,
|
||
url = {https://arxiv.org/abs/1603.01445},
|
||
doi = {10.1016/j.entcs.2016.09.043},
|
||
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},
|
||
doi={10.1214/aoms/1177700153},
|
||
publisher={Institute of Mathematical Statistics},
|
||
url={https://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 = {https://dx.doi.org/10.4204/EPTCS.57.11},
|
||
doi = {10.4204/EPTCS.57.11},
|
||
timestamp = {Mon, 28 Oct 2013 16:56:55 +0100},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/journals/corr/abs-1107-1206},
|
||
bibsource = {dblp computer science bibliography, https://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}}
|
||
|
||
inproceedings{LarsenS89,
|
||
author = {Larsen, Kim Guldstrand and
|
||
Skou, Arne},
|
||
title = {Bisimulation through Probabilistic Testing},
|
||
booktitle = popl89,
|
||
pages = {344--352},
|
||
year = {1989},
|
||
url = {https://doi.acm.org/10.1145/75277.75307},
|
||
doi = {10.1016/0890-5401(91)90030-6},
|
||
timestamp = {Mon, 21 May 2012 16:19:51 +0200},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/conf/popl/LarsenS89},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@article{LarsenS89,
|
||
author = {Larsen, Kim Guldstrand and
|
||
Skou, Arne},
|
||
title = {Bisimulation through Probabilistic Testing},
|
||
journal = {Information and Computation},
|
||
volume = {94},
|
||
number = {1},
|
||
pages = {1--28},
|
||
year = {1991},
|
||
doi = {10.1016/0890-5401(91)90030-6},
|
||
url = {https://www.sciencedirect.com/science/article/pii/0890540191900306},
|
||
publisher = elsevier,
|
||
timestamp = {Mon, 21 May 2012 16:19:51 +0200},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/conf/popl/LarsenS89},
|
||
bibsource = {dblp computer science bibliography, https://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},
|
||
url={https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.3664}
|
||
}
|
||
|
||
@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 = {https://oa.upm.es/23088/1/FEDERICO_OLMEDO.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 = {https://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 = {https://dblp.uni-trier.de/rec/bib/journals/jct/AharoniBGPS11},
|
||
bibsource = {dblp computer science bibliography, https://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},
|
||
doi={10.4230/LIPIcs.CALCO.2015.156},
|
||
url = {https://drops.dagstuhl.de/opus/volltexte/2015/5532},
|
||
}
|
||
|
||
@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,
|
||
url={https://eudml.org/doc/113445}
|
||
}
|
||
|
||
@book {RudinPMA,
|
||
AUTHOR = {Rudin, Walter},
|
||
TITLE = {Principles of Mathematical Analysis},
|
||
EDITION = {Third},
|
||
SERIES = {International Series in Pure and Applied Mathematics},
|
||
PUBLISHER = mcgh,
|
||
YEAR = {1976},
|
||
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,
|
||
doi = {10.1145/3110254},
|
||
pages = {10:1--10:29},
|
||
url = {https://dl.acm.org/citation.cfm?id=3110254}
|
||
}
|
||
|
||
@book{Kleinberg:2005:AD:1051910,
|
||
author = {Kleinberg, Jon and Tardos, Eva},
|
||
title = {Algorithm Design},
|
||
year = {2005},
|
||
isbn = {0321295358},
|
||
publisher = aw,
|
||
}
|
||
|
||
@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 {Horn} 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 {Horn} 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 = {https://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 = {https://doi.acm.org/10.1145/1168857.1168907},
|
||
doi = {10.1145/1168857.1168907},
|
||
timestamp = {Tue, 15 May 2007 09:22:32 +0200},
|
||
biburl =
|
||
{https://dblp.dagstuhl.de/rec/bib/conf/asplos/Solar-LezamaTBSS06},
|
||
bibsource = {dblp computer science bibliography,
|
||
https://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 = {https://doi.acm.org/10.1145/1706299.1706337},
|
||
doi = {10.1145/1706299.1706337},
|
||
acmid = {1706337},
|
||
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},
|
||
keywords = {games, horn clauses, program synthesis, proof rules, reactive synthesis, static analysis},
|
||
}
|
||
|
||
@inproceedings{beyene2013solving,
|
||
title={Solving existentially quantified {Horn} 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 = {https://doi.acm.org/10.1145/800017.800528},
|
||
doi = {10.1145/800017.800528},
|
||
timestamp = {Mon, 21 May 2012 16:19:51 +0200},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/conf/popl/MacQueenPS84},
|
||
bibsource = {dblp computer science bibliography, https://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 = {https://dblp.uni-trier.de/rec/bib/conf/lics/AbadiP90},
|
||
bibsource = {dblp computer science bibliography, https://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 = {https://arxiv.org/abs/1603.00570},
|
||
timestamp = {Sat, 02 Apr 2016 11:49:48 +0200},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/journals/corr/Shamir16},
|
||
bibsource = {dblp computer science bibliography, https://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 =
|
||
{https://dblp2.uni-trier.de/rec/bib/series/ncs/Jansen13},
|
||
bibsource = {dblp computer science bibliography,
|
||
https://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},
|
||
doi = {10.1162/153244302760200704},
|
||
url = {https://www.jmlr.org/papers/v2/bousquet02a.html}
|
||
}
|
||
|
||
@inproceedings{GomulkiewiczKK03,
|
||
author = {Marcin Gomulkiewicz and
|
||
Marek Klonowski and
|
||
Miroslaw Kutylowski},
|
||
title = {Rapid Mixing and Security of {Chaum}'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: {Theory} 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 = {https://eprint.iacr.org/2012/363},
|
||
timestamp = {Fri, 28 Mar 2014 20:49:29 +0100},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/journals/iacr/CanteautFNPRV12},
|
||
bibsource = {dblp computer science bibliography, https://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: {Categorical} 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},
|
||
URL = {https://pages.uoregon.edu/dlevin/MARKOV/markovmixing.pdf}
|
||
}
|
||
|
||
@book{Villani08,
|
||
title={Optimal Transport: {Old} and New},
|
||
author={Villani, C{\'e}dric},
|
||
year={2008},
|
||
doi={10.1007/978-3-540-71050-9},
|
||
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: {Towards} usable verification},
|
||
booktitle = pldi14,
|
||
pages = {32},
|
||
year = {2014}
|
||
}
|
||
|
||
@article{GodlinS13,
|
||
author = {Benny Godlin and
|
||
Ofer Strichman},
|
||
title = {Regression verification: {Proving} 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 = {https://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 = {https://dblp.uni-trier.de/rec/bib/conf/esop/FosterKMR016},
|
||
bibsource = {dblp computer science bibliography, https://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 = {https://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 = {https://dblp.uni-trier.de/rec/bib/conf/esop/KaminskiKMO16},
|
||
bibsource = {dblp computer science bibliography, https://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 = {https://eprint.iacr.org/2016/912},
|
||
timestamp = {Fri, 14 Oct 2016 13:36:12 +0200},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/journals/iacr/BartheDFGSS16},
|
||
bibsource = {dblp computer science bibliography, https://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: {Quantifying} 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 = {https://dx.doi.org/10.1109/TCAD.2015.2424951},
|
||
doi = {10.1109/TCAD.2015.2424951},
|
||
timestamp = {Thu, 03 Nov 2016 07:24:15 +0100},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/journals/tcad/EldibWTS15},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@inproceedings{DBLP:conf/crypto/IshaiSW03,
|
||
author = {Yuval Ishai and
|
||
Amit Sahai and
|
||
David Wagner},
|
||
title = {Private Circuits: {Securing} Hardware against Probing Attacks},
|
||
booktitle = crypto03,
|
||
series = lncs,
|
||
volume = {2729},
|
||
pages = {463--481},
|
||
publisher = springer,
|
||
year = {2003},
|
||
url = {https://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 = {https://dblp.uni-trier.de/rec/bib/conf/crypto/IshaiSW03},
|
||
bibsource = {dblp computer science bibliography, https://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 = {https://www.jmlr.org/papers/v6/elisseeff05a.html},
|
||
timestamp = {Wed, 21 Feb 2007 09:15:37 +0100},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/journals/jmlr/ElisseeffEP05},
|
||
bibsource = {dblp computer science bibliography, https://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 = {https://dx.doi.org/10.1137/1.9781611974331.ch36},
|
||
doi = {10.1137/1.9781611974331.ch36},
|
||
timestamp = {Thu, 07 Apr 2016 12:20:54 +0200},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/conf/soda/PanageasSV16},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@inproceedings{Vishnoi15,
|
||
author = {Nisheeth K. Vishnoi},
|
||
title = {The Speed of Evolution},
|
||
booktitle = soda15,
|
||
pages = {1590--1601},
|
||
year = {2015},
|
||
url = {https://dx.doi.org/10.1137/1.9781611973730.105},
|
||
doi = {10.1137/1.9781611973730.105},
|
||
timestamp = {Wed, 28 Jan 2015 11:43:18 +0100},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/conf/soda/Vishnoi15},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@article{diaconis91,
|
||
author = {Diaconis, Persi and Stroock, Daniel},
|
||
citeulike-article-id = {8906755},
|
||
citeulike-linkout-0 = {https://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 {Markov} Chains},
|
||
url = {https://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 = {https://dx.doi.org/10.1137/0218077},
|
||
doi = {10.1137/0218077},
|
||
timestamp = {Mon, 12 Sep 2011 16:10:07 +0200},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/journals/siamcomp/JerrumS89},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@article{DBLP:journals/rsa/KumarR01,
|
||
author = {V. S. Anil Kumar and H. Ramesh},
|
||
title = {Coupling vs. Conductance for the {Jerrum-Sinclair} Chain},
|
||
journal = {Random Structures and Algorithms},
|
||
volume = {18},
|
||
number = {1},
|
||
pages = {1--17},
|
||
year = {2001},
|
||
url = {https://hariharan-ramesh.com/papers/mcmc.pdf},
|
||
publisher = {Wiley}
|
||
}
|
||
|
||
@inproceedings{HardtRS16,
|
||
author = {Moritz Hardt and
|
||
Ben Recht and
|
||
Yoram Singer},
|
||
title = {Train Faster, Generalize Better: {Stability} of Stochastic Gradient Descent},
|
||
booktitle = icml16,
|
||
series = pmlr,
|
||
volume = {48},
|
||
pages = {1225--1234},
|
||
year = {2016},
|
||
archivePrefix = "arXiv",
|
||
eprint = {1509.01240},
|
||
primaryClass = "cs.LG",
|
||
url={https://arxiv.org/abs/1603.01445}
|
||
}
|
||
|
||
@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 = {https://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 = {https://doi.acm.org/10.1145/800070.802188},
|
||
doi = {10.1145/800070.802188},
|
||
timestamp = {Sun, 21 May 2017 00:22:29 +0200},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/conf/stoc/DeBakkerZ82},
|
||
bibsource = {dblp computer science bibliography, https://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 = {https://dblp.uni-trier.de/rec/bib/journals/tcs/ArnoldN80},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@book{brooks2011handbook,
|
||
title={Handbook of {Markov} Chain {Monte} {Carlo}},
|
||
author={Brooks, Steve and Gelman, Andrew and Jones, Galin and Meng,
|
||
Xiao-Li},
|
||
year={2011},
|
||
publisher={CRC press}
|
||
}
|
||
|
||
@inproceedings{sato2016approximate,
|
||
title={Approximate Relational {Hoare} Logic for Continuous Random Samplings},
|
||
author={Sato, Tetsuya},
|
||
booktitle=mfps16,
|
||
year={2016},
|
||
doi={10.1016/j.entcs.2016.09.043},
|
||
url={https://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 = {https://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 = {https://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 = {https://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="https://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 = {https://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 = {https://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 = {https://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 = "https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 {Kripke} 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 = {https://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 = {https://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 = {https://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 = {https://dx.doi.org/10.1109/LICS.2011.38},
|
||
}
|
||
|
||
@article{csiszarS04,
|
||
url = {https://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 = {https://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 = {https://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 = {https://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 = {https://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 {Feistel} 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 = {({Not} 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={https://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 = {https://arxiv.org/abs/1508.07306},
|
||
timestamp = {Tue, 01 Sep 2015 14:42:40 +0200},
|
||
biburl = {https://dblp.uni-trier.de/rec/bib/journals/corr/ChenM15e},
|
||
bibsource = {dblp computer science bibliography, https://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 = "https://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 {Hoare}'s Logic: {A} Survey--Part {I}},
|
||
journal = toplas,
|
||
volume = {3},
|
||
number = {4},
|
||
year = {1981},
|
||
issn = {0164-0925},
|
||
pages = {431--483},
|
||
numpages = {53},
|
||
url = {https://doi.acm.org/10.1145/357146.357150},
|
||
doi = {10.1145/357146.357150},
|
||
acmid = {357150},
|
||
}
|
||
|
||
@article{APT198383,
|
||
title = "Ten years of {Hoare}'s logic: {A} survey--Part {II}: Nondeterminism",
|
||
journal = tcs,
|
||
volume = "28",
|
||
number = "1",
|
||
pages = "83--109",
|
||
year = "1983",
|
||
issn = "0304-3975",
|
||
doi = "https://dx.doi.org/10.1016/0304-3975(83)90066-X",
|
||
url = "https://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 = "https://dx.doi.org/10.1016/j.tcs.2006.12.036",
|
||
url = "https://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},
|
||
doi = {10.1145/2676726.2677005},
|
||
url = {https://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},
|
||
url={https://arxiv.org/abs/1505.02642}
|
||
}
|
||
|
||
@article{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},
|
||
journal=pvldb,
|
||
note=vldb14,
|
||
volume={7},
|
||
number={8},
|
||
pages={637--648},
|
||
year={2014},
|
||
doi={10.14778/2732296.2732300},
|
||
url={https://www.vldb.org/pvldb/vol7/p637-proserpio.pdf},
|
||
}
|
||
|
||
@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 = {https://madsbuch.com/thesis},
|
||
year = 2017
|
||
}
|
||
|
||
@article{Callahan1988,
|
||
author="Callahan, David and Kennedy, Ken",
|
||
title="Compiling Programs for Distributed-Memory Multiprocessors",
|
||
journal="The Journal of Supercomputing",
|
||
year="1988",
|
||
month=oct,
|
||
volume="2",
|
||
number="2",
|
||
pages="151--169",
|
||
abstract="We describe a new approach to programming distributed-memory
|
||
computers. Rather than having each node in the system explicitly programmed, we
|
||
derive an efficient message-passing program from a sequential shared-memory
|
||
program annotated with directions on how elements of shared arrays are
|
||
distributed to processors. This article describes one possible input language
|
||
for describing distributions and then details the compilation process and the
|
||
optimization necessary to generate an efficient program.",
|
||
issn="1573-0484",
|
||
doi="10.1007/BF00128175",
|
||
url="https://doi.org/10.1007/BF00128175",
|
||
publisher=springer
|
||
}
|
||
|
||
@inproceedings{Chatterjee:2016:AAQ:2837614.2837639,
|
||
author = {Chatterjee, Krishnendu and Fu, Hongfei and Novotn\'{y}, Petr and Hasheminezhad, Rouzbeh},
|
||
title = {Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs},
|
||
booktitle = popl16,
|
||
year = {2016},
|
||
isbn = {978-1-4503-3549-2},
|
||
pages = {327--342},
|
||
numpages = {16},
|
||
url = {https://doi.acm.org/10.1145/2837614.2837639},
|
||
doi = {10.1145/2837614.2837639},
|
||
acmid = {2837639},
|
||
keywords = {Concentration, Probabilistic Programs, Ranking Supermartingale, Termination},
|
||
}
|
||
|
||
@inproceedings{Chatterjee2016,
|
||
author= {Chatterjee, Krishnendu and Fu, Hongfei and Goharshady, Amir
|
||
Kafshdar},
|
||
title= {Termination Analysis of Probabilistic Programs through {Positivstellensatz's}},
|
||
bookTitle=cav16,
|
||
year="2016",
|
||
publisher=springer,
|
||
series=lncs,
|
||
volume=9779,
|
||
pages="3--22",
|
||
isbn="978-3-319-41528-4",
|
||
doi="10.1007/978-3-319-41528-4_1",
|
||
url="https://doi.org/10.1007/978-3-319-41528-4_1"
|
||
}
|
||
|
||
@inproceedings{Chatterjee:2017:SIP:3009837.3009873,
|
||
author = {Chatterjee, Krishnendu and Novotn\'{y}, Petr and \v{Z}ikeli\'{c}, {\DH}or{\dj}e},
|
||
title = {Stochastic Invariants for Probabilistic Termination},
|
||
booktitle = popl17,
|
||
year = {2017},
|
||
isbn = {978-1-4503-4660-3},
|
||
pages = {145--160},
|
||
numpages = {16},
|
||
url = {https://doi.acm.org/10.1145/3009837.3009873},
|
||
doi = {10.1145/3009837.3009873},
|
||
acmid = {3009873},
|
||
keywords = {Concentration, Martingales, Probabilistic Programs, Termination},
|
||
}
|
||
|
||
@article{mciver2016new,
|
||
title={A New Rule for Almost-Certain Termination},
|
||
author={McIver, Annabelle and
|
||
Morgan, Carroll and
|
||
Kaminski, Benjamin Lucien and
|
||
Katoen, {Joost}-{Pieter}},
|
||
journal = pacmpl,
|
||
volume = {1},
|
||
number = {POPL},
|
||
note="To appear at " # popl18,
|
||
year={2018},
|
||
url={https://arxiv.org/abs/1612.01091}
|
||
}
|
||
|
||
@article{deng2009kantorovich,
|
||
title={The {Kantorovich} Metric in Computer Science: {A} Brief Survey},
|
||
author={Deng, Yuxin and Du, Wenjie},
|
||
journal=entcs,
|
||
volume={253},
|
||
number={3},
|
||
pages={73--82},
|
||
year={2009},
|
||
publisher=elsevier,
|
||
doi={10.1016/j.entcs.2009.10.006},
|
||
url={https://www.sciencedirect.com/science/article/pii/S1571066109004265}
|
||
}
|
||
|
||
@article{ghosh2012universally,
|
||
title={Universally Utility-Maximizing Privacy Mechanisms},
|
||
author={Ghosh, Arpita and Roughgarden, Tim and Sundararajan, Mukund},
|
||
journal=siamjc,
|
||
volume={41},
|
||
number={6},
|
||
pages={1673--1693},
|
||
year={2012},
|
||
doi={10.1137/09076828X},
|
||
url={https://arxiv.org/abs/0811.2841}
|
||
}
|
||
|
||
@misc{Shoup:2004,
|
||
author = {Victor Shoup},
|
||
title = {Sequences of Games: {A} Tool for Taming Complexity in Security Proofs},
|
||
howpublished = {Cryptology ePrint Archive, Report 2004/332},
|
||
year = {2004},
|
||
url = {https://eprint.iacr.org/2004/332},
|
||
}
|
||
|
||
@article{HallWassermanRinaldo,
|
||
author = {Hall, Robert and
|
||
Wasserman, Larry and
|
||
Rinaldo, Alessandro},
|
||
title = {Random Differential Privacy},
|
||
journal = jpc,
|
||
volume = {4},
|
||
issue = {2},
|
||
number = {3},
|
||
url = {https://repository.cmu.edu/jpc/vol4/iss2/3},
|
||
year = 2013}
|
||
|
||
|
||
|
||
@article{DBLP:journals/rsa/HayesV07,
|
||
author = {Thomas P. Hayes and
|
||
Eric Vigoda},
|
||
title = {Variable Length Path Coupling},
|
||
journal = {Random Structures and Algorithms},
|
||
volume = {31},
|
||
number = {3},
|
||
pages = {251--272},
|
||
year = {2007},
|
||
url = {https://doi.org/10.1002/rsa.20166},
|
||
doi = {10.1002/rsa.20166},
|
||
publisher = {Wiley},
|
||
timestamp = {Fri, 26 May 2017 22:50:39 +0200},
|
||
biburl = {https://dblp.org/rec/bib/journals/rsa/HayesV07},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@article{DBLP:journals/rsa/ProppW96,
|
||
author = {James Gary Propp and
|
||
David Bruce Wilson},
|
||
title = {Exact Sampling with Coupled {Markov} Chains and Applications to Statistical Mechanics},
|
||
journal = {Random Structures and Algorithms},
|
||
volume = {9},
|
||
number = {1-2},
|
||
pages = {223--252},
|
||
year = {1996},
|
||
url = {https://doi.org/10.1002/(SICI)1098-2418(199608/09)9:1/2<223::AID-RSA14>3.0.CO;2-O},
|
||
publisher = {Wiley},
|
||
doi = {10.1002/(SICI)1098-2418(199608/09)9:1/2<223::AID-RSA14>3.0.CO;2-O},
|
||
timestamp = {Fri, 26 May 2017 22:50:39 +0200},
|
||
biburl = {https://dblp.org/rec/bib/journals/rsa/ProppW96},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@InProceedings{fijalkow_et_al:LIPIcs:2017:7368,
|
||
author ={Nathana{\"e}l Fijalkow and Bartek Klin and Prakash Panangaden},
|
||
title ={Expressiveness of Probabilistic Modal Logics, Revisited},
|
||
booktitle =icalp17,
|
||
pages ={105:1--105:12},
|
||
series =lipics,
|
||
ISBN ={978-3-95977-041-5},
|
||
ISSN ={1868-8969},
|
||
year ={2017},
|
||
volume ={80},
|
||
editor ={Ioannis Chatzigiannakis and Piotr Indyk and Fabian Kuhn and Anca Muscholl},
|
||
publisher =dagstuhl,
|
||
address ={Dagstuhl, Germany},
|
||
URL ={https://drops.dagstuhl.de/opus/volltexte/2017/7368},
|
||
URN ={urn:nbn:de:0030-drops-73683},
|
||
doi ={10.4230/LIPIcs.ICALP.2017.105},
|
||
annote ={Keywords: probabilistic modal logic, probabilistic bisimulation, probabilistic simulation}
|
||
}
|
||
|
||
@article{DESHARNAIS2002163,
|
||
title = {Bisimulation for Labelled {Markov} Processes},
|
||
journal = {Information and Computation},
|
||
volume = {179},
|
||
number = {2},
|
||
pages = {163--193},
|
||
year = {2002},
|
||
issn = {0890-5401},
|
||
doi = {10.1006/inco.2001.2962},
|
||
url = {https://www.sciencedirect.com/science/article/pii/S0890540101929621},
|
||
author = {Jos{\'e}e Desharnais and Abbas Edalat and Prakash Panangaden},
|
||
publisher=elsevier
|
||
}
|
||
|
||
@article{DESHARNAIS2003160,
|
||
title = {Approximating Labelled {Markov} Processes},
|
||
journal = {Information and Computation},
|
||
volume = {184},
|
||
number = {1},
|
||
pages = {160--200},
|
||
year = {2003},
|
||
issn = {0890-5401},
|
||
doi = {10.1016/S0890-5401(03)00051-8},
|
||
url = {https://www.sciencedirect.com/science/article/pii/S0890540103000518},
|
||
author = {Jos{\'e}e Desharnais and Vineet Gupta and Radha Jagadeesan and Prakash Panangaden}
|
||
}
|
||
|
||
@article{DESHARNAIS2004323,
|
||
title = {Metrics for Labelled {Markov} Processes},
|
||
journal = tcs,
|
||
volume = {318},
|
||
number = {3},
|
||
pages = {323--354},
|
||
year = {2004},
|
||
issn = {0304-3975},
|
||
publisher = elsevier,
|
||
doi = {10.1016/j.tcs.2003.09.013},
|
||
url = {https://www.sciencedirect.com/science/article/pii/S0304397503006042},
|
||
author = {Jos{\'e}e Desharnais and Vineet Gupta and Radha Jagadeesan and Prakash Panangaden},
|
||
keywords = {Labelled Markov processes, Metric, Process Algebra}
|
||
}
|
||
|
||
@inproceedings{vanBreugel2001a,
|
||
author={van Breugel, Franck and Worrell, James},
|
||
title={An Algorithm for Quantitative Verification of Probabilistic Transition Systems},
|
||
booktitle=concur01,
|
||
year={2001},
|
||
publisher=springer,
|
||
pages={336--350},
|
||
series=lncs,
|
||
volume=2154,
|
||
isbn={978-3-540-44685-9},
|
||
doi={10.1007/3-540-44685-0_23},
|
||
url={https://doi.org/10.1007/3-540-44685-0_23}
|
||
}
|
||
|
||
@inproceedings{vanBreugel2001b,
|
||
author={van Breugel, Franck and Worrell, James},
|
||
editor={Orejas, Fernando and Spirakis, Paul G. and van Leeuwen, Jan},
|
||
title={Towards Quantitative Verification of Probabilistic Transition Systems},
|
||
bookTitle=icalp01,
|
||
year={2001},
|
||
publisher=springer,
|
||
pages={421--432},
|
||
series=lncs,
|
||
volume=2076,
|
||
isbn={978-3-540-48224-6},
|
||
doi={10.1007/3-540-48224-5_35},
|
||
url={https://doi.org/10.1007/3-540-48224-5_35}
|
||
}
|
||
|
||
@phdthesis{desharnais1999labelled,
|
||
title={Labelled {Markov} Processes},
|
||
author={Desharnais, Jos{\'e}e},
|
||
school={{McGill} University},
|
||
url={www.collectionscanada.gc.ca/obj/s4/f2/dsk1/tape3/PQDD_0031/NQ64546.pdf},
|
||
year={1999}
|
||
}
|
||
|
||
@article{DBLP:journals/njc/SegalaL95,
|
||
author = {Roberto Segala and
|
||
Nancy A. Lynch},
|
||
title = {Probabilistic Simulations for Probabilistic Processes},
|
||
journal = {Nordic Journal of Computing},
|
||
volume = {2},
|
||
number = {2},
|
||
pages = {250--273},
|
||
year = {1995},
|
||
doi = {doi.org/10.1007/BFb0015027},
|
||
timestamp = {Wed, 14 Jan 2004 15:33:50 +0100},
|
||
biburl = {https://dblp.org/rec/bib/journals/njc/SegalaL95},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@book{durrett2010probability,
|
||
title={Probability: theory and examples},
|
||
author={Durrett, Rick},
|
||
year={2010},
|
||
publisher=cup
|
||
}
|
||
|
||
@article{azuma1967weighted,
|
||
title={Weighted sums of certain dependent random variables},
|
||
author={Azuma, Kazuoki},
|
||
journal={Tohoku Mathematical Journal},
|
||
series=2,
|
||
volume={19},
|
||
number={3},
|
||
pages={357--367},
|
||
year={1967},
|
||
publisher={Mathematical Institute, Tohoku University}
|
||
}
|