Add EC and IJCAI submissions to site.
This commit is contained in:
Justin Hsu
parent
4177507f99
commit
77864bdec1
548
bibs/myrefs.bib
548
bibs/myrefs.bib
|
|
@ -76,18 +76,6 @@
|
||||||
year = {2010},
|
year = {2010},
|
||||||
}
|
}
|
||||||
|
|
||||||
@inproceedings{DMNS06,
|
|
||||||
title = {Calibrating noise to sensitivity in private data analysis},
|
|
||||||
author = {Cynthia Dwork and
|
|
||||||
Frank McSherry and
|
|
||||||
Kobbi Nissim and
|
|
||||||
Adam Smith},
|
|
||||||
pages = {265--284},
|
|
||||||
url = {http://dx.doi.org/10.1007/11681878_14},
|
|
||||||
booktitle = tcc06,
|
|
||||||
year = {2006}
|
|
||||||
}
|
|
||||||
|
|
||||||
@article{GS99,
|
@article{GS99,
|
||||||
title = {Walrasian equilibrium with gross substitutes},
|
title = {Walrasian equilibrium with gross substitutes},
|
||||||
author = {Gul, Faruk and Stacchetti, Ennio},
|
author = {Gul, Faruk and Stacchetti, Ennio},
|
||||||
|
|
@ -111,21 +99,6 @@
|
||||||
year = {2013},
|
year = {2013},
|
||||||
}
|
}
|
||||||
|
|
||||||
@inproceedings{HKR12,
|
|
||||||
title = {Distributed private heavy hitters},
|
|
||||||
author = {Hsu, Justin and
|
|
||||||
Khanna, Sanjeev and
|
|
||||||
Roth, Aaron},
|
|
||||||
booktitle = icalp12,
|
|
||||||
pages = {461--472},
|
|
||||||
year = {2012},
|
|
||||||
publisher = springer,
|
|
||||||
url = {http://arxiv.org/abs/1202.4910},
|
|
||||||
jh = yes,
|
|
||||||
slides = yes,
|
|
||||||
eprint = yes
|
|
||||||
}
|
|
||||||
|
|
||||||
@inproceedings{HRU13,
|
@inproceedings{HRU13,
|
||||||
title = {Differential privacy for the analyst via private equilibrium computation},
|
title = {Differential privacy for the analyst via private equilibrium computation},
|
||||||
author = {Hsu, Justin and
|
author = {Hsu, Justin and
|
||||||
|
|
@ -263,6 +236,19 @@
|
||||||
docs = yes,
|
docs = yes,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@inproceedings{GGHHP13,
|
||||||
|
title = {Automatic sensitivity analysis using linear dependent types},
|
||||||
|
author = {Gaboardi, Marco and
|
||||||
|
Gallego Arias, Emilio Jes{\'u}s and
|
||||||
|
Haeberlen, Andreas and
|
||||||
|
Hsu, Justin and
|
||||||
|
Pierce, Benjamin C},
|
||||||
|
url = {http://fopara2013.cs.unibo.it/paper_8.pdf},
|
||||||
|
booktitle = fopara,
|
||||||
|
year = {2013},
|
||||||
|
jh = yes,
|
||||||
|
}
|
||||||
|
|
||||||
@inproceedings{GHHNP13,
|
@inproceedings{GHHNP13,
|
||||||
title = {Linear dependent types for differential privacy},
|
title = {Linear dependent types for differential privacy},
|
||||||
author = {Gaboardi, Marco and
|
author = {Gaboardi, Marco and
|
||||||
|
|
@ -278,19 +264,6 @@
|
||||||
docs = yes,
|
docs = yes,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
@inproceedings{GGHHP13,
|
|
||||||
title = {Automatic sensitivity analysis using linear dependent types},
|
|
||||||
author = {Gaboardi, Marco and
|
|
||||||
Gallego Arias, Emilio Jes{\'u}s and
|
|
||||||
Haeberlen, Andreas and
|
|
||||||
Hsu, Justin and
|
|
||||||
Pierce, Benjamin C},
|
|
||||||
url = {http://fopara2013.cs.unibo.it/paper_8.pdf},
|
|
||||||
booktitle = fopara,
|
|
||||||
year = {2013},
|
|
||||||
jh = yes,
|
|
||||||
}
|
|
||||||
@inproceedings{HLM12,
|
@inproceedings{HLM12,
|
||||||
title = {A Simple and Practical Algorithm for Differentially Private Data Release},
|
title = {A Simple and Practical Algorithm for Differentially Private Data Release},
|
||||||
author = {Moritz Hardt and Katrina Ligett and Frank {McSherry}},
|
author = {Moritz Hardt and Katrina Ligett and Frank {McSherry}},
|
||||||
|
|
@ -300,6 +273,22 @@
|
||||||
year = 2012
|
year = 2012
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@inproceedings{HKR12,
|
||||||
|
title = {Distributed private heavy hitters},
|
||||||
|
author = {Hsu, Justin and
|
||||||
|
Khanna, Sanjeev and
|
||||||
|
Roth, Aaron},
|
||||||
|
booktitle = icalp12,
|
||||||
|
pages = {461--472},
|
||||||
|
year = {2012},
|
||||||
|
publisher = springer,
|
||||||
|
url = {http://arxiv.org/abs/1202.4910},
|
||||||
|
jh = yes,
|
||||||
|
slides = yes,
|
||||||
|
eprint = yes
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
@inproceedings{Ullman13,
|
@inproceedings{Ullman13,
|
||||||
title = {Answering $n^{2+ o(1)}$ counting queries with differential
|
title = {Answering $n^{2+ o(1)}$ counting queries with differential
|
||||||
privacy is hard},
|
privacy is hard},
|
||||||
|
|
@ -1621,6 +1610,7 @@ year = {2014}
|
||||||
volume={55},
|
volume={55},
|
||||||
number={2},
|
number={2},
|
||||||
year={2006},
|
year={2006},
|
||||||
|
pages={242--269},
|
||||||
url={http://www.ime.usp.br/~yw/papers/games/goldberg2008-competitive-auctions.pdf},
|
url={http://www.ime.usp.br/~yw/papers/games/goldberg2008-competitive-auctions.pdf},
|
||||||
publisher={Elsevier}
|
publisher={Elsevier}
|
||||||
}
|
}
|
||||||
|
|
@ -1782,8 +1772,7 @@ year = {2014}
|
||||||
year = {2015},
|
year = {2015},
|
||||||
url = {http://arxiv.org/abs/1407.6845},
|
url = {http://arxiv.org/abs/1407.6845},
|
||||||
jh = yes,
|
jh = yes,
|
||||||
eprint = yes,
|
eprint = yes
|
||||||
slides = yes,
|
|
||||||
}
|
}
|
||||||
|
|
||||||
@inproceedings{IOh01,
|
@inproceedings{IOh01,
|
||||||
|
|
@ -2020,25 +2009,13 @@ year = {2014}
|
||||||
Gallego Arias, Emilio Jes{\'u}s and
|
Gallego Arias, Emilio Jes{\'u}s and
|
||||||
Hsu, Justin},
|
Hsu, Justin},
|
||||||
title = {Really naturally linear indexed type-checking},
|
title = {Really naturally linear indexed type-checking},
|
||||||
booktitle = {Implementation of Functional Languages (IFL), Boston, Massachusetts},
|
booktitle = {Proceedings of Implementation of Functional Languages (IFL), Boston, Massachusetts},
|
||||||
year = {2014},
|
year = {2014},
|
||||||
url = {http://www.cis.upenn.edu/~justhsu/docs/dfuzztc.pdf},
|
url = {http://www.cis.upenn.edu/~justhsu/docs/dfuzztc.pdf},
|
||||||
jh = yes,
|
jh = yes,
|
||||||
docs = yes,
|
docs = yes,
|
||||||
}
|
}
|
||||||
|
|
||||||
@unpublished{HHRW15,
|
|
||||||
author = {Hsu, Justin and
|
|
||||||
Huang, Zhiyi and
|
|
||||||
Roth, Aaron and
|
|
||||||
Wu, Zhiwei Steven},
|
|
||||||
title = {Jointly private convex programming},
|
|
||||||
year = {2015},
|
|
||||||
url = {http://arxiv.org/abs/1411.0998},
|
|
||||||
jh = yes,
|
|
||||||
eprint = yes
|
|
||||||
}
|
|
||||||
|
|
||||||
@article{LovaszLocal,
|
@article{LovaszLocal,
|
||||||
title={Problems and results on 3-chromatic hypergraphs and some related
|
title={Problems and results on 3-chromatic hypergraphs and some related
|
||||||
questions},
|
questions},
|
||||||
|
|
@ -2124,18 +2101,469 @@ year = {2014}
|
||||||
}
|
}
|
||||||
|
|
||||||
@unpublished{GHaccuracy,
|
@unpublished{GHaccuracy,
|
||||||
author = {Gaboardi, Marco and
|
author = {Marco Gaboardi and
|
||||||
Hsu, Justin },
|
Justin Hsu},
|
||||||
title = {A theory {AB} toolbox},
|
title = {A Theory {AB} Toolbox},
|
||||||
year = {2015},
|
year = {2015},
|
||||||
jh = yes,
|
jh = yes,
|
||||||
docs = yes
|
docs = yes
|
||||||
}
|
}
|
||||||
|
|
||||||
@unpublished{HsuTaxes,
|
@unpublished{HsuTaxes,
|
||||||
author = {Hsu, Justin},
|
author = {Justin Hsu},
|
||||||
title = {Death, taxes, and formal verification},
|
title = {Death, Taxes, and Formal Verification},
|
||||||
year = {2015},
|
year = {2015},
|
||||||
jh = yes,
|
jh = yes,
|
||||||
docs = yes
|
docs = yes
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@InProceedings{Necula97,
|
||||||
|
author = "G. C. Necula",
|
||||||
|
title = "Proof-carrying code",
|
||||||
|
booktitle = popl97,
|
||||||
|
year = "1997",
|
||||||
|
pages = "106--119",
|
||||||
|
publisher = {ACM}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{Barthe11,
|
||||||
|
Author = {Gilles Barthe and Benjamin Gr{\'e}goire and Sylvain Heraud and Santiago Zanella B{\'e}guelin},
|
||||||
|
Booktitle = crypto11,
|
||||||
|
Pages = {71-90},
|
||||||
|
Title = {Computer-Aided Security Proofs for the Working Cryptographer},
|
||||||
|
Year = {2011}}
|
||||||
|
@inproceedings{flanagan2001,
|
||||||
|
title={Avoiding exponential explosion: Generating compact
|
||||||
|
verification conditions},
|
||||||
|
author={Flanagan, Cormac and Saxe, James B},
|
||||||
|
booktitle=popl01,
|
||||||
|
pages={193--205},
|
||||||
|
year={2001},
|
||||||
|
publisher={ACM}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{BartheDGKSS13,
|
||||||
|
author = {Gilles Barthe and
|
||||||
|
Fran{\c{c}}ois Dupressoir and
|
||||||
|
Benjamin Gr{\'{e}}goire and
|
||||||
|
C{\'{e}}sar Kunz and
|
||||||
|
Benedikt Schmidt and
|
||||||
|
Pierre{-}Yves Strub},
|
||||||
|
title = {Easy{C}rypt: {A} Tutorial},
|
||||||
|
booktitle = {Foundations of Security Analysis and Design {VII} - {FOSAD} 2012/2013
|
||||||
|
Tutorial Lectures},
|
||||||
|
pages = {146--166},
|
||||||
|
series = {LNCS},
|
||||||
|
year = {2014},
|
||||||
|
volume = {8604},
|
||||||
|
publisher = {Springer}
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{Hoare69,
|
||||||
|
author = {C. A. R. Hoare},
|
||||||
|
title = {An Axiomatic Basis for Computer Programming},
|
||||||
|
journal = cacm,
|
||||||
|
year = {1969},
|
||||||
|
volume = {12},
|
||||||
|
number = {10}
|
||||||
|
}
|
||||||
|
|
||||||
|
@incollection{Floyd67,
|
||||||
|
author = {Floyd, Robert W.},
|
||||||
|
booktitle = {Symposium on {A}pplied {M}athematics},
|
||||||
|
publisher = {Amer. Math. Soc.},
|
||||||
|
title = {{Assigning meanings to programs}},
|
||||||
|
year = {1967}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
@article{Cook:1978,
|
||||||
|
Author = {Cook, S.},
|
||||||
|
Journal = siamjc,
|
||||||
|
Number = {1},
|
||||||
|
Pages = {70-90},
|
||||||
|
Title = {Soundness and Completeness of an Axiom System for Program Verification},
|
||||||
|
Volume = {7},
|
||||||
|
Year = {1978}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{Clarkson:2008,
|
||||||
|
Author = {Clarkson, M.R. and Schneider, F.B.},
|
||||||
|
Booktitle = csf08,
|
||||||
|
Publisher = {IEEE},
|
||||||
|
Title = {Hyperproperties},
|
||||||
|
Year = {2008}
|
||||||
|
}
|
||||||
|
|
||||||
|
@InProceedings{Turing:1949,
|
||||||
|
author = "Alan M. Turing",
|
||||||
|
title = "Checking a Large Routine",
|
||||||
|
pages = "67--69",
|
||||||
|
year = "1949",
|
||||||
|
URL = "http://www.turingarchive.org/browse.php/B/8",
|
||||||
|
booktitle = "{Report on a Conference on High Speed Automatic
|
||||||
|
Computation, June 1949}",
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
@inproceedings{HM07,
|
||||||
|
title={The communication complexity of uncoupled nash equilibrium procedures},
|
||||||
|
author={Hart, Sergiu and Mansour, Yishay},
|
||||||
|
booktitle=stoc07,
|
||||||
|
pages={345--353},
|
||||||
|
year={2007},
|
||||||
|
organization={ACM}
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{DGP09,
|
||||||
|
title={The complexity of computing a Nash equilibrium},
|
||||||
|
author={Daskalakis, Constantinos and Goldberg, Paul W and Papadimitriou, Christos H},
|
||||||
|
journal=siamjc,
|
||||||
|
volume={39},
|
||||||
|
number={1},
|
||||||
|
pages={195--259},
|
||||||
|
year={2009},
|
||||||
|
publisher={SIAM}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{CS02,
|
||||||
|
title={Complexity of mechanism design},
|
||||||
|
author={Conitzer, Vincent and Sandholm, Tuomas},
|
||||||
|
booktitle=uai02,
|
||||||
|
pages={103--110},
|
||||||
|
year={2002},
|
||||||
|
organization={Morgan Kaufmann Publishers Inc.}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{San03,
|
||||||
|
title={Automated mechanism design: A new application area for search algorithms},
|
||||||
|
author={Sandholm, Tuomas},
|
||||||
|
booktitle=cp03,
|
||||||
|
pages={19--36},
|
||||||
|
year={2003},
|
||||||
|
organization={Springer}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{BP14,
|
||||||
|
title={Verifiably Truthful Mechanisms},
|
||||||
|
author={Br{\^a}nzei, Simina and Procaccia, Ariel D},
|
||||||
|
booktitle=itcs14,
|
||||||
|
year={2014}
|
||||||
|
}
|
||||||
|
|
||||||
|
@phdthesis{Con06,
|
||||||
|
title={Computational aspects of preference aggregation},
|
||||||
|
author={Conitzer, Vincent},
|
||||||
|
year={2006},
|
||||||
|
school={IBM}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{HKM11,
|
||||||
|
title={Bayesian incentive compatibility via matchings},
|
||||||
|
author={Hartline, Jason D and Kleinberg, Robert and Malekian, Azarakhsh},
|
||||||
|
booktitle=soda11,
|
||||||
|
pages={734--747},
|
||||||
|
year={2011},
|
||||||
|
organization={SIAM}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{BH11,
|
||||||
|
title={Bayesian incentive compatibility via fractional assignments},
|
||||||
|
author={Bei, Xiaohui and Huang, Zhiyi},
|
||||||
|
booktitle=soda11,
|
||||||
|
pages={720--733},
|
||||||
|
year={2011},
|
||||||
|
organization={SIAM}
|
||||||
|
}
|
||||||
|
|
||||||
|
@book{Rou05,
|
||||||
|
title={Selfish routing and the price of anarchy},
|
||||||
|
author={Roughgarden, Tim},
|
||||||
|
volume={174},
|
||||||
|
year={2005},
|
||||||
|
publisher={MIT press Cambridge}
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{Chadha:2007,
|
||||||
|
Author = {Chadha, R. and Cruz-Filipe, L. and Mateus, P. and Sernadas, A.},
|
||||||
|
Journal = tcs,
|
||||||
|
Number = {1-2},
|
||||||
|
Title = {Reasoning about probabilistic sequential programs},
|
||||||
|
Volume = {379},
|
||||||
|
Year = {2007}}
|
||||||
|
|
||||||
|
@article{Morgan:1996,
|
||||||
|
author = {C Morgan and
|
||||||
|
A Mc{I}ver and
|
||||||
|
K Seidel},
|
||||||
|
title = {Probabilistic Predicate Transformers},
|
||||||
|
journal = toplas,
|
||||||
|
volume = {18},
|
||||||
|
number = {3},
|
||||||
|
year = {1996}
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{Kozen:1985,
|
||||||
|
author = {D. Kozen},
|
||||||
|
title = {A Probabilistic {PDL}},
|
||||||
|
journal = jcss,
|
||||||
|
volume = {30},
|
||||||
|
number = {2},
|
||||||
|
year = {1985}
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{Chadha:2007,
|
||||||
|
Author = {Chadha, R. and Cruz-Filipe, L. and Mateus, P. and Sernadas, A.},
|
||||||
|
Journal = tcs,
|
||||||
|
Number = {1-2},
|
||||||
|
Title = {Reasoning about probabilistic sequential programs},
|
||||||
|
Volume = {379},
|
||||||
|
Year = {2007}}
|
||||||
|
|
||||||
|
@article{Morgan:1996,
|
||||||
|
author = {C Morgan and
|
||||||
|
A Mc{I}ver and
|
||||||
|
K Seidel},
|
||||||
|
title = {Probabilistic Predicate Transformers},
|
||||||
|
journal = toplas,
|
||||||
|
volume = {18},
|
||||||
|
number = {3},
|
||||||
|
year = {1996}
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{Kozen:1985,
|
||||||
|
author = {D. Kozen},
|
||||||
|
title = {A Probabilistic {PDL}},
|
||||||
|
journal = jcss,
|
||||||
|
volume = {30},
|
||||||
|
number = {2},
|
||||||
|
year = {1985}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{TGV09,
|
||||||
|
year={2009},
|
||||||
|
booktitle={Declarative Agent Languages and Technologies VI},
|
||||||
|
volume={5397},
|
||||||
|
series={LNCS},
|
||||||
|
doi={10.1007/978-3-540-93920-7_13},
|
||||||
|
title={Abstracting and Verifying Strategy-Proofness for Auction Mechanisms},
|
||||||
|
publisher={Springer Berlin Heidelberg},
|
||||||
|
author={Tadjouddine, Emmanuel M. and Guerin, Frank and Vasconcelos, Wamberto},
|
||||||
|
pages={197-214},
|
||||||
|
language={English}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
@inproceedings{DBLP:conf/ceemas/TadjouddineG07,
|
||||||
|
author = {Emmanuel M Tadjouddine and
|
||||||
|
Frank Guerin},
|
||||||
|
title = {Verifying Dominant Strategy Equilibria in Auctions},
|
||||||
|
booktitle = {{CEEMAS 2007}},
|
||||||
|
year = {2007},
|
||||||
|
pages = {288--297},
|
||||||
|
publisher = {Springer},
|
||||||
|
series = {LNCS},
|
||||||
|
volume = {4696},
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{DBLP:journals/corr/BaiTG14,
|
||||||
|
author = {Wei Bai and
|
||||||
|
Emmanuel M Tadjouddine and
|
||||||
|
Yu Guo},
|
||||||
|
title = {Enabling Automatic Certification of Online Auctions},
|
||||||
|
booktitle = {{FESCA 2014}},
|
||||||
|
series = {EPTCS},
|
||||||
|
volume = {147},
|
||||||
|
year = {2014},
|
||||||
|
pages = {123--132},
|
||||||
|
url = {http://dx.doi.org/10.4204/EPTCS.147.9},
|
||||||
|
}
|
||||||
|
|
||||||
|
@incollection{DBLP:conf/mkm/0002CKMRWW13,
|
||||||
|
author = {Christoph Lange and
|
||||||
|
Marco B Caminati and
|
||||||
|
Manfred Kerber and
|
||||||
|
Till Mossakowski and
|
||||||
|
Colin Rowat and
|
||||||
|
Makarius Wenzel and
|
||||||
|
Wolfgang Windsteiger},
|
||||||
|
title = {A Qualitative Comparison of the Suitability of Four Theorem
|
||||||
|
Provers for Basic Auction Theory},
|
||||||
|
booktitle={Intelligent Computer Mathematics},
|
||||||
|
publisher = {Springer},
|
||||||
|
series = {Lecture Notes in Computer Science},
|
||||||
|
volume = {7961},
|
||||||
|
year = {2013},
|
||||||
|
pages = {200--215},
|
||||||
|
url = {http://dx.doi.org/10.1007/978--3-642--39320--4_13},
|
||||||
|
publisher={Springer}
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{DBLP:journals/ipl/Vestergaard06,
|
||||||
|
author = {Ren{\'e} Vestergaard},
|
||||||
|
title = {A constructive approach to sequential Nash equilibria},
|
||||||
|
journal = {Inf. Process. Lett.},
|
||||||
|
volume = {97},
|
||||||
|
number = {2},
|
||||||
|
year = {2006},
|
||||||
|
pages = {46--51},
|
||||||
|
url = {http://dx.doi.org/10.1016/j.ipl.2005.09.010},
|
||||||
|
bibsource = {DBLP, http://dblp.uni-trier.de}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{DBLP:conf/aaai/WooldridgeADH07,
|
||||||
|
author = {Michael Wooldridge and
|
||||||
|
Thomas {A}gotnes and
|
||||||
|
Paul E. Dunne and
|
||||||
|
Wiebe van der Hoek},
|
||||||
|
title = {Logic for Automated Mechanism Design---{A} Progress Report},
|
||||||
|
booktitle = aaai07,
|
||||||
|
pages = {9--17},
|
||||||
|
year = {2007},
|
||||||
|
}
|
||||||
|
|
||||||
|
@Article{Alur:2002:ATT,
|
||||||
|
author = "Rajeev Alur and Thomas A. Henzinger and Orna
|
||||||
|
Kupferman",
|
||||||
|
title = "Alternating-time temporal logic",
|
||||||
|
journal = jacm,
|
||||||
|
volume = "49",
|
||||||
|
number = "5",
|
||||||
|
pages = "672--713",
|
||||||
|
month = sep,
|
||||||
|
year = "2002",
|
||||||
|
journal-url = "http://portal.acm.org/browse_dl.cfm?idx=J401",
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{DBLP:conf/itp/GonthierAABCGRMOBPRSTT13,
|
||||||
|
author = {Georges Gonthier and
|
||||||
|
Andrea Asperti and
|
||||||
|
Jeremy Avigad and
|
||||||
|
Yves Bertot and
|
||||||
|
Cyril Cohen and
|
||||||
|
Fran{\c{c}}ois Garillot and
|
||||||
|
St{\'{e}}phane Le Roux and
|
||||||
|
Assia Mahboubi and
|
||||||
|
Russell O'Connor and
|
||||||
|
Sidi Ould Biha and
|
||||||
|
Ioana Pasca and
|
||||||
|
Laurence Rideau and
|
||||||
|
Alexey Solovyev and
|
||||||
|
Enrico Tassi and
|
||||||
|
Laurent Th{\'{e}}ry},
|
||||||
|
title = {A Machine-Checked Proof of the Odd Order Theorem},
|
||||||
|
booktitle = {Interactive Theorem Proving (ITP)},
|
||||||
|
pages = {163--179},
|
||||||
|
year = {2013},
|
||||||
|
doi = {10.1007/978-3-642-39634-2_14},
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{vickrey61,
|
||||||
|
title={Counterspeculation, auctions, and competitive sealed tenders},
|
||||||
|
author={Vickrey, William},
|
||||||
|
journal={The Journal of finance},
|
||||||
|
volume={16},
|
||||||
|
number={1},
|
||||||
|
pages={8--37},
|
||||||
|
year={1961},
|
||||||
|
publisher={Wiley Online Library}
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{clarke71,
|
||||||
|
title={Multipart pricing of public goods},
|
||||||
|
author={Clarke, Edward H},
|
||||||
|
journal={Public choice},
|
||||||
|
volume={11},
|
||||||
|
number={1},
|
||||||
|
pages={17--33},
|
||||||
|
year={1971},
|
||||||
|
publisher={Springer}
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{groves73,
|
||||||
|
title={Incentives in teams},
|
||||||
|
author={Groves, Theodore},
|
||||||
|
journal={Econometrica: Journal of the Econometric Society},
|
||||||
|
pages={617--631},
|
||||||
|
year={1973}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{Bellare:2006,
|
||||||
|
address = {Heidelberg},
|
||||||
|
author = {Bellare, Mihir and Rogaway, Phillip},
|
||||||
|
booktitle = eucrypt06,
|
||||||
|
pages = {409--426},
|
||||||
|
publisher = {Springer},
|
||||||
|
series = {Lecture Notes in Computer Science},
|
||||||
|
title = {The Security of Triple Encryption and a Framework for
|
||||||
|
Code-Based Game-Playing Proofs},
|
||||||
|
volume = {4004},
|
||||||
|
year = {2006},
|
||||||
|
url = {https://www.iacr.org/archive/eurocrypt2006/40040415/40040415.pdf}
|
||||||
|
}
|
||||||
|
|
||||||
|
@misc{Halevi:2005,
|
||||||
|
author = {Halevi, Shai},
|
||||||
|
howpublished = {Cryptology ePrint Archive, Report 2005/181},
|
||||||
|
title = {A plausible approach to computer-aided cryptographic proofs},
|
||||||
|
year = {2005},
|
||||||
|
url = {https://eprint.iacr.org/2005/181.pdf}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
@misc{Shoup:2004,
|
||||||
|
author = {Shoup, Victor},
|
||||||
|
howpublished = {Cryptology ePrint Archive, Report 2004/332},
|
||||||
|
title = {Sequences of games: a tool for taming complexity in security proofs},
|
||||||
|
year = {2004}
|
||||||
|
}
|
||||||
|
|
||||||
|
@unpublished{Naumann:2009,
|
||||||
|
author = {Naumann, David A},
|
||||||
|
title = {Theory for software verification},
|
||||||
|
year = {2009},
|
||||||
|
url = {http://www.cs.stevens.edu/~naumann/publications/theoryverif.pdf}
|
||||||
|
}
|
||||||
|
|
||||||
|
@incollection{handbook-sat,
|
||||||
|
title = {Satisfiability Modulo Theories},
|
||||||
|
author = {Barrett, Clark and Sebastini, Roberto and Seshia, Sanjit A and
|
||||||
|
Tinelli, Cesare},
|
||||||
|
booktitle = {Handbook of satisfiability},
|
||||||
|
volume = {185},
|
||||||
|
year = {2009},
|
||||||
|
publisher = {IOS press},
|
||||||
|
}
|
||||||
|
|
||||||
|
@unpublished{HHRW15,
|
||||||
|
author = {Hsu, Justin and
|
||||||
|
Huang, Zhiyi and
|
||||||
|
Roth, Aaron and
|
||||||
|
Wu, Zhiwei Steven},
|
||||||
|
title = {Jointly private convex programming},
|
||||||
|
year = {2015},
|
||||||
|
url = {http://arxiv.org/abs/1411.0998},
|
||||||
|
jh = yes,
|
||||||
|
eprint = yes
|
||||||
|
}
|
||||||
|
|
||||||
|
@unpublished{AHJ15,
|
||||||
|
title = {Online Assignment with Heterogeneous Tasks and Deadlines},
|
||||||
|
author = {Assadi, Sepehr and Hsu, Justin and Jabbari, Shahin},
|
||||||
|
year = {2015},
|
||||||
|
jh = yes
|
||||||
|
}
|
||||||
|
|
||||||
|
@unpublished{HKM-verif,
|
||||||
|
title = {Computer-aided verification in mechanism design},
|
||||||
|
author = {Barthe, Gilles and
|
||||||
|
Gaboardi, Marco and
|
||||||
|
Gallego Arias, Emilio Jes{\'u}s and
|
||||||
|
Hsu, Justin and
|
||||||
|
Roth, Aaron and
|
||||||
|
Strub, Pierre-Yves},
|
||||||
|
year = {2015},
|
||||||
|
url = {http://arxiv.org/abs/1502.04052},
|
||||||
|
jh = yes,
|
||||||
|
eprint = yes
|
||||||
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,7 +1,7 @@
|
||||||
|
+ **02/2015** Our paper **Computer-aided verification in mechanism design** has
|
||||||
|
been uploaded to `arxiv`.
|
||||||
+ **01/2015** I will be visiting **IMDEA Software** in Madrid until early March.
|
+ **01/2015** I will be visiting **IMDEA Software** in Madrid until early March.
|
||||||
+ **01/2015** Our abstract **Death, Taxes, and Formal Verification** has been uploaded.
|
+ **01/2015** Our abstract **Death, Taxes, and Formal Verification** has been uploaded.
|
||||||
+ **01/2015** Our paper **A Theory AB Toolbox** has been uploaded.
|
+ **01/2015** Our paper **A Theory AB Toolbox** has been uploaded.
|
||||||
+ **11/2014** Our paper **Jointly private convex programming** has been uploaded to
|
+ **11/2014** Our paper **Jointly private convex programming** has been uploaded to
|
||||||
`arXiv`.
|
`arXiv`.
|
||||||
+ **09/2014** Our paper **Higher-order refinement types for mechanism design and
|
|
||||||
differential privacy** has been accepted to POPL 2015!
|
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue