IDEAS home Printed from https://ideas.repec.org/p/bir/birmec/15-08.html
   My bibliography  Save this paper

Sound Auction Specification and Implementation

Author

Listed:
  • Marco B Caminati
  • Manfred Kerber
  • Christoph Lange
  • Colin Rowat

Abstract

We introduce 'formal methods' of mechanized reasoning from computer science to address two problems in auction design and practice: is a given auction design soundly specified, possessing its intended properties; and, is the design faithfully implemented when actually run? Failure on either front can be hugely costly in large auctions. In the familiar setting of the combinatorial Vickrey auction, we use a mechanized reasoner, Isabelle, to first ensure that the auction has a set of desired properties (e.g. allocating all items at non-negative prices), and to then generate verified executable code directly from the specified design. Having established the expected results in a known context, we intend next to use formal methods to verify new auction designs.

Suggested Citation

  • Marco B Caminati & Manfred Kerber & Christoph Lange & Colin Rowat, 2015. "Sound Auction Specification and Implementation," Discussion Papers 15-08, Department of Economics, University of Birmingham.
    • Handle: RePEc:bir:birmec:15-08
    as

    Download full text from publisher

    File URL: https://repec.cal.bham.ac.uk/pdf/15-08.pdf
    Download Restriction: no
    ---><---

    References listed on IDEAS

    as
    1. Andrei A. Kirilenko & Andrew W. Lo, 2013. "Moore's Law versus Murphy's Law: Algorithmic Trading and Its Discontents," Journal of Economic Perspectives, American Economic Association, vol. 27(2), pages 51-72, Spring.
    2. Orhan Ayg?n & Tayfun S?nmez, 2013. "Matching with Contracts: Comment," American Economic Review, American Economic Association, vol. 103(5), pages 2050-2051, August.
    3. John William Hatfield & Paul R. Milgrom, 2005. "Matching with Contracts," American Economic Review, American Economic Association, vol. 95(4), pages 913-935, September.
    4. Kerber, Manfred & Lange, Christoph & Rowat, Colin, 2016. "An introduction to mechanized reasoning," Journal of Mathematical Economics, Elsevier, vol. 66(C), pages 26-39.
    Full references (including those not matched with items on IDEAS)

    Citations

    Citations are extracted by the CitEc Project, subscribe to its RSS feed for this item.
    as


    Cited by:

    1. Suneel Sarswat & Abhishek Kr Singh, 2020. "Formally Verified Trades in Financial Markets," Papers 2007.10805, arXiv.org.
    2. Suneel Sarswat & Abhishek Kr Singh, 2019. "Formal verification of trading in financial markets," Papers 1907.07885, arXiv.org.
    3. Kerber, Manfred & Lange, Christoph & Rowat, Colin, 2016. "An introduction to mechanized reasoning," Journal of Mathematical Economics, Elsevier, vol. 66(C), pages 26-39.

    Most related items

    These are the items that most often cite the same works as this one and are cited by the same works as this one.
    1. Chen, Peter & Egesdal, Michael & Pycia, Marek & Yenmez, M. Bumin, 2016. "Median stable matchings in two-sided markets," Games and Economic Behavior, Elsevier, vol. 97(C), pages 64-69.
    2. Kadam, Sangram Vilasrao, 2017. "Unilateral substitutability implies substitutable completability in many-to-one matching with contracts," Games and Economic Behavior, Elsevier, vol. 102(C), pages 56-68.
    3. Ehlers, Lars & Klaus, Bettina, 2016. "Object allocation via deferred-acceptance: Strategy-proofness and comparative statics," Games and Economic Behavior, Elsevier, vol. 97(C), pages 128-146.
    4. Hirata, Daisuke & Kasuya, Yusuke, 2014. "Cumulative offer process is order-independent," Economics Letters, Elsevier, vol. 124(1), pages 37-40.
    5. Avataneo, Michelle & Turhan, Bertan, 2021. "Slot-specific priorities with capacity transfers," Games and Economic Behavior, Elsevier, vol. 129(C), pages 536-548.
    6. Afacan, Mustafa Oǧuz, 2020. "Graduate admission with financial support," Journal of Mathematical Economics, Elsevier, vol. 87(C), pages 114-127.
    7. Hatfield, John William & Kominers, Scott Duke, 2017. "Contract design and stability in many-to-many matching," Games and Economic Behavior, Elsevier, vol. 101(C), pages 78-97.
    8. Aygün, Orhan & Turhan, Bertan, 2020. "Dynamic reserves in matching markets," Journal of Economic Theory, Elsevier, vol. 188(C).
    9. Antonio Romero-Medina & Matteo Triossi, 2023. "Take-it-or-leave-it contracts in many-to-many matching markets," Economic Theory, Springer;Society for the Advancement of Economic Theory (SAET), vol. 75(2), pages 591-623, February.
    10. Mustafa Oǧuz Afacan, 2016. "Characterizations of the cumulative offer process," Social Choice and Welfare, Springer;The Society for Social Choice and Welfare, vol. 47(3), pages 531-542, October.
    11. Hans Gersbach & Hans Haller & Hideo Konishi, 2015. "Household formation and markets," Economic Theory, Springer;Society for the Advancement of Economic Theory (SAET), vol. 59(3), pages 461-507, August.
    12. Hafalir, Isa E. & Kojima, Fuhito & Yenmez, M. Bumin, 2022. "Interdistrict school choice: A theory of student assignment," Journal of Economic Theory, Elsevier, vol. 201(C).
    13. Kerber, Manfred & Lange, Christoph & Rowat, Colin, 2016. "An introduction to mechanized reasoning," Journal of Mathematical Economics, Elsevier, vol. 66(C), pages 26-39.
    14. Tello, Benjamín, 2016. "Matching with contracts, substitutes and two-unit demand," Economics Letters, Elsevier, vol. 146(C), pages 85-88.
    15. Klijn, Flip & Yazıcı, Ayşe, 2014. "A many-to-many ‘rural hospital theorem’," Journal of Mathematical Economics, Elsevier, vol. 54(C), pages 63-73.
    16. Zhang, Jun, 2016. "On sufficient conditions for the existence of stable matchings with contracts," Economics Letters, Elsevier, vol. 145(C), pages 230-234.
    17. Doğan, Battal & Yenmez, M. Bumin, 2019. "Unified versus divided enrollment in school choice: Improving student welfare in Chicago," Games and Economic Behavior, Elsevier, vol. 118(C), pages 366-373.
    18. Kojima, Fuhito & Tamura, Akihisa & Yokoo, Makoto, 2018. "Designing matching mechanisms under constraints: An approach from discrete convex analysis," Journal of Economic Theory, Elsevier, vol. 176(C), pages 803-833.
    19. Tayfun Sönmez & M. Bumin Yenmez, 2019. "Constitutional Implementation of Vertical and Horizontal Reservations in India: A Unified Mechanism for Civil Service Allocation and College Admissions," Boston College Working Papers in Economics 978, Boston College Department of Economics.
    20. Aygün, Orhan & Turhan, Bertan, 2019. "Matching with Generalized Lexicographic Choice Rules," ISU General Staff Papers 20191101070000, Iowa State University, Department of Economics.

    More about this item

    Keywords

    formal proof; mechanized reasoning; auction theory;
    All these keywords.

    JEL classification:

    • B41 - Schools of Economic Thought and Methodology - - Economic Methodology - - - Economic Methodology
    • C63 - Mathematical and Quantitative Methods - - Mathematical Methods; Programming Models; Mathematical and Simulation Modeling - - - Computational Techniques
    • C88 - Mathematical and Quantitative Methods - - Data Collection and Data Estimation Methodology; Computer Programs - - - Other Computer Software
    • D44 - Microeconomics - - Market Structure, Pricing, and Design - - - Auctions

    Statistics

    Access and download statistics

    Corrections

    All material on this site has been provided by the respective publishers and authors. You can help correct errors and omissions. When requesting a correction, please mention this item's handle: RePEc:bir:birmec:15-08. See general information about how to correct material in RePEc.

    If you have authored this item and are not yet registered with RePEc, we encourage you to do it here. This allows to link your profile to this item. It also allows you to accept potential citations to this item that we are uncertain about.

    If CitEc recognized a bibliographic reference but did not link an item in RePEc to it, you can help with this form .

    If you know of missing items citing this one, you can help us creating those links by adding the relevant references in the same way as above, for each refering item. If you are a registered author of this item, you may also want to check the "citations" tab in your RePEc Author Service profile, as there may be some citations waiting for confirmation.

    For technical questions regarding this item, or to correct its authors, title, abstract, bibliographic or download information, contact: Oleksandr Talavera (email available below). General contact details of provider: https://edirc.repec.org/data/debhauk.html .

    Please note that corrections may take a couple of weeks to filter through the various RePEc services.

    IDEAS is a RePEc service. RePEc uses bibliographic data supplied by the respective publishers.