Satisfiability modulo theories, Handbook of satisfiability, 2009. ,
URL : https://hal.archives-ouvertes.fr/hal-01095009
Computer-Aided Security Proofs for the Working Cryptographer, IACR International Cryptology Conference (CRYPTO), pp.71-90, 2011. ,
DOI : 10.1007/978-3-642-22792-9_5
URL : https://hal.archives-ouvertes.fr/hal-01112075
EasyCrypt: A Tutorial, Foundations of Security Analysis and Design VII -FOSAD 2012/2013 Tutorial Lectures, pp.146-166, 2014. ,
DOI : 10.1007/978-3-642-22792-9_5
URL : https://hal.archives-ouvertes.fr/hal-01114366
Higher-order approximate relational refinement types for mechanism design and differential privacy, ACM SIGPLAN?SIGACT Symposium on Principles of Programming Languages (POPL), pp.55-68, 2015. ,
DOI : 10.1145/2775051.2677000
URL : http://arxiv.org/abs/1407.6845
The Security of Triple Encryption and a Framework??for??Code-Based??Game-Playing??Proofs, Lecture Notes in Computer Science, vol.4004, pp.409-426, 2006. ,
DOI : 10.1007/11761679_25
Verifiably Truthful Mechanisms, Proceedings of the 2015 Conference on Innovations in Theoretical Computer Science, ITCS '15 ,
DOI : 10.1145/2688073.2688098
Sound auction specification and implementation, ACM SIGecom Conference on Economics and Computation (EC), pp.547-564, 2015. ,
DOI : 10.1145/2764468.2764511
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.696.5096
The price of anarchy of finite congestion games, Proceedings of the thirty-seventh annual ACM symposium on Theory of computing , STOC '05, pp.67-73, 2005. ,
DOI : 10.1145/1060590.1060600
Multipart pricing of public goods, Public Choice, vol.7, issue.1, pp.17-33, 1971. ,
DOI : 10.1007/BF01726210
Computational aspects of preference aggregation, IBM, 2006. ,
Complexity of mechanism design, Conference on Uncertainty in Artificial Intelligence (UAI), pp.103-110, 2002. ,
The Complexity of Computing a Nash Equilibrium, SIAM Journal on Computing, vol.39, issue.1, pp.195-259, 2009. ,
DOI : 10.1137/070699652
Competitive auctions, Games and Economic Behavior, vol.55, issue.2, pp.242-269, 2006. ,
DOI : 10.1016/j.geb.2006.02.003
Common enrollment, parents, and school choice: Early evidence from denver and new orleans. making school choice work series, Center on Reinventing Public Education (CRPE), 2015. ,
Incentives in Teams, Econometrica, vol.41, issue.4, pp.617-631, 1973. ,
DOI : 10.2307/1914085
A plausible approach to computer-aided cryptographic proofs, Cryptology ePrint Archive Report, vol.181, 2005. ,
The communication complexity of uncoupled nash equilibrium procedures, Proceedings of the thirty-ninth annual ACM symposium on Theory of computing , STOC '07, pp.345-353, 2007. ,
DOI : 10.1145/1250790.1250843
Bayesian incentive compatibility via matchings, ACM?SIAM Symposium on Discrete Algorithms (SODA), pp.734-747, 2011. ,
DOI : 10.1016/j.geb.2015.02.002
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.193.9148
strategic behavior' in a strategy-proof environment. Working paper, 2016. ,
An introduction to mechanized reasoning. CoRR, abs, 1603. ,
DOI : 10.1016/j.jmateco.2016.06.005
URL : http://doi.org/10.1016/j.jmateco.2016.06.005
Obviously Strategy-Proof Mechanisms, SSRN Electronic Journal ,
DOI : 10.2139/ssrn.2560028
Deffered acceptance auctions and radio spectrum reallocation, 2014. ,
DOI : 10.1145/2600057.2602834
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.473.8144
A note on testing truthfulness, Electronic Colloquium on Computational Complexity (ECCC), number 130, 2005. ,
Selfish Routing and the Price of Anarchy, 2005. ,
DOI : 10.1017/CBO9781316779309.012
Automated Mechanism Design: A New Application Area for Search Algorithms, International Conference on Principles and Practice of Constraint Programming (CP), pp.19-36, 2003. ,
DOI : 10.1007/978-3-540-45193-8_2
COUNTERSPECULATION, AUCTIONS, AND COMPETITIVE SEALED TENDERS, The Journal of Finance, vol.16, issue.1, pp.8-37, 1961. ,
DOI : 10.1111/j.1540-6261.1961.tb02789.x
Alternating-time temporal logic, Journal of the ACM, vol.49, issue.5, pp.672-713, 2002. ,
A Proof-Carrying Code Approach to Certificate Auction Mechanisms, FACS, pp.23-40, 2013. ,
DOI : 10.1007/978-3-319-07602-7_4
Formal certification of code-based cryptographic proofs, ACM SIGPLAN?SIGACT Symposium on Principles of Programming Languages (POPL), 2009. ,
DOI : 10.1145/1480881.1480894
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.220.4653
EasyCrypt: A Tutorial, Foundations of Security Analysis and Design VII -FOSAD 2012/2013 Tutorial Lectures, pp.146-166, 2014. ,
DOI : 10.1007/978-3-642-22792-9_5
URL : https://hal.archives-ouvertes.fr/hal-01114366
Higher-order approximate relational refinement types for mechanism design and differential privacy, ACM SIGPLAN?SIGACT Symposium on Principles of Programming Languages (POPL), pp.55-68, 2015. ,
DOI : 10.1145/2775051.2677000
URL : http://arxiv.org/abs/1407.6845
Simple relational correctness proofs for static analyses and program transformations, ACM SIGPLAN?SIGACT Symposium on Principles of Programming Languages (POPL), pp.14-25, 2004. ,
DOI : 10.1145/964001.964003
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.4900
Reasoning about probabilistic sequential programs, Theoretical Computer Science, vol.379, issue.1-2, pp.142-165, 2007. ,
DOI : 10.1016/j.tcs.2007.02.040
URL : http://doi.org/10.1016/j.tcs.2007.02.040
Multipart pricing of public goods, Public Choice, vol.7, issue.1, pp.17-33, 1971. ,
DOI : 10.1007/BF01726210
Soundness and Completeness of an Axiom System for Program Verification, SIAM Journal on Computing, vol.7, issue.1, pp.70-90, 1978. ,
DOI : 10.1137/0207005
Avoiding exponential explosion: Generating compact verification conditions, ACM SIGPLAN?SIGACT Symposium on Principles of Programming Languages (POPL), pp.193-205, 2001. ,
Assigning meanings to programs, Symposium on Applied Mathematics. Amer, 1967. ,
DOI : 10.1007/978-94-011-1793-7_4
A machinechecked proof of the odd order theorem, Interactive Theorem Proving (ITP), pp.163-179, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00816699
Incentives in Teams, Econometrica, vol.41, issue.4, pp.617-631, 1973. ,
DOI : 10.2307/1914085
An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, 1969. ,
DOI : 10.1007/978-94-011-1793-7_5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.116.2392
A probabilistic PDL, Proceedings of the fifteenth annual ACM symposium on Theory of computing , STOC '83, 1985. ,
DOI : 10.1145/800061.808758
URL : http://doi.org/10.1016/0022-0000(85)90012-1
A Typed Truthful Language for One-dimensional Truthful Mechanism Design, 2008. ,
Probabilistic predicate transformers, ACM Transactions on Programming Languages and Systems, vol.18, issue.3, pp.325-353, 1996. ,
DOI : 10.1145/229542.229547
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.166.127
Truthful approximation mechanisms for restricted combinatorial auctions, Games and Economic Behavior, vol.64, issue.2, pp.612-631, 2008. ,
DOI : 10.1016/j.geb.2007.12.009
Verifying Dominant Strategy Equilibria in Auctions, CEEMAS 2007, pp.288-297, 2007. ,
DOI : 10.1007/978-3-540-75254-7_29
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.100.7128
Abstracting and Verifying Strategy-Proofness for Auction Mechanisms, Declarative Agent Languages and Technologies VI, pp.197-214, 2009. ,
DOI : 10.1109/32.730543
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.140.9737
Checking a large routine, Report on a Conference on High Speed Automatic Computation, pp.67-69, 1949. ,
COUNTERSPECULATION, AUCTIONS, AND COMPETITIVE SEALED TENDERS, The Journal of Finance, vol.16, issue.1, pp.8-37, 1961. ,
DOI : 10.1111/j.1540-6261.1961.tb02789.x
Logic for automated mechanism design?A progress report, AAAI Conference on Artificial Intelligence, pp.9-17, 2007. ,