IDEAS home Printed from https://ideas.repec.org/p/arx/papers/2007.10805.html
   My bibliography  Save this paper

Formally Verified Trades in Financial Markets

Author

Listed:
  • Suneel Sarswat
  • Abhishek Kr Singh

Abstract

We introduce a formal framework for analyzing trades in financial markets. These days, all big exchanges use computer algorithms to match buy and sell requests and these algorithms must abide by certain regulatory guidelines. For example, market regulators enforce that a matching produced by exchanges should be fair, uniform and individual rational. To verify these properties of trades, we first formally define these notions in a theorem prover and then develop many important results about matching demand and supply. Finally, we use this framework to verify properties of two important classes of double sided auction mechanisms. All the definitions and results presented in this paper are completely formalized in the Coq proof assistant without adding any additional axioms to it.

Suggested Citation

  • Suneel Sarswat & Abhishek Kr Singh, 2020. "Formally Verified Trades in Financial Markets," Papers 2007.10805, arXiv.org.
    • Handle: RePEc:arx:papers:2007.10805
    as

    Download full text from publisher

    File URL: http://arxiv.org/pdf/2007.10805
    File Function: Latest version
    Download Restriction: no
    ---><---

    References listed on IDEAS

    as
    1. 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.
    2. McAfee, R. Preston, 1992. "A dominant strategy double auction," Journal of Economic Theory, Elsevier, vol. 56(2), pages 434-450, April.
    3. Jinzhong Niu & Simon Parsons, 2013. "Maximizing Matching in Double-sided Auctions," Papers 1304.3135, arXiv.org.
    Full references (including those not matched with items on IDEAS)

    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. Suneel Sarswat & Abhishek Kr Singh, 2019. "Formal verification of trading in financial markets," Papers 1907.07885, arXiv.org.
    2. Scott Fay & Robert Zeithammer, 2017. "Bidding for Bidders? How the Format for Soliciting Supplier Participation in NYOP Auctions Impacts Channel Profit," Management Science, INFORMS, vol. 63(12), pages 4324-4344, December.
    3. Tafreshian, Amirmahdi & Masoud, Neda, 2022. "A truthful subsidy scheme for a peer-to-peer ridesharing market with incomplete information," Transportation Research Part B: Methodological, Elsevier, vol. 162(C), pages 130-161.
    4. Loertscher, Simon & Mezzetti, Claudio, 2021. "A dominant strategy, double clock auction with estimation-based tatonnement," Theoretical Economics, Econometric Society, vol. 16(3), July.
    5. Rustichini, Aldo & Satterthwaite, Mark A & Williams, Steven R, 1994. "Convergence to Efficiency in a Simple Market with Incomplete Information," Econometrica, Econometric Society, vol. 62(5), pages 1041-1063, September.
    6. Dütting, Paul & Talgam-Cohen, Inbal & Roughgarden, Tim, 2017. "Modularity and greed in double auctions," LSE Research Online Documents on Economics 83199, London School of Economics and Political Science, LSE Library.
    7. Kiho Yoon, 2021. "Robust double auction mechanisms," Papers 2102.00669, arXiv.org, revised May 2022.
    8. Xuanming Su, 2010. "Optimal Pricing with Speculators and Strategic Consumers," Management Science, INFORMS, vol. 56(1), pages 25-40, January.
    9. Satterthwaite, Mark A. & Williams, Steven R. & Zachariadis, Konstantinos E., 2014. "Optimality versus practicality in market design: A comparison of two double auctions," Games and Economic Behavior, Elsevier, vol. 86(C), pages 248-263.
    10. Jesse A. Schwartz & Quan Wen, 2008. "A Revelation Principle for Dominant Strategy Implementation," Vanderbilt University Department of Economics Working Papers 0819, Vanderbilt University Department of Economics.
    11. Loertscher, Simon & Marx, Leslie M., 2020. "A dominant-strategy asset market mechanism," Games and Economic Behavior, Elsevier, vol. 120(C), pages 1-15.
    12. Soumendu Sarkar, 2022. "Optimal mechanism for land acquisition," Review of Economic Design, Springer;Society for Economic Design, vol. 26(1), pages 87-116, March.
    13. Kong, Xiang T.R. & Kang, Kai & Zhong, Ray Y. & Luo, Hao & Xu, Su Xiu, 2021. "Cyber physical system-enabled on-demand logistics trading," International Journal of Production Economics, Elsevier, vol. 233(C).
    14. Cheng, Meng & Xu, Su Xiu & Huang, George Q., 2016. "Truthful multi-unit multi-attribute double auctions for perishable supply chain trading," Transportation Research Part E: Logistics and Transportation Review, Elsevier, vol. 93(C), pages 21-37.
    15. Baliga Sandeep & Vohra Rakesh, 2003. "Market Research and Market Design," The B.E. Journal of Theoretical Economics, De Gruyter, vol. 3(1), pages 1-27, August.
    16. Yoon, Kiho, 2008. "The participatory Vickrey-Clarke-Groves mechanism," Journal of Mathematical Economics, Elsevier, vol. 44(3-4), pages 324-336, February.
    17. Drexl, Moritz & Kleiner, Andreas, 2015. "Optimal private good allocation: The case for a balanced budget," Games and Economic Behavior, Elsevier, vol. 94(C), pages 169-181.
    18. Miyashita, Kazuo, 2015. "Developing an Online Market Mechanism for Trading Perishable Agricultural Commodities," 2015 Conference, August 9-14, 2015, Milan, Italy 212470, International Association of Agricultural Economists.
    19. Athanasiou, E. & Dey, S. & Valletta, G., 2012. "On sharing the benefits of communication," Research Memorandum 016, Maastricht University, Maastricht Research School of Economics of Technology and Organization (METEOR).
    20. Babaioff, Moshe & Nisan, Noam & Pavlov, Elan, 2009. "Mechanisms for a spatially distributed market," Games and Economic Behavior, Elsevier, vol. 66(2), pages 660-684, July.

    More about this item

    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:arx:papers:2007.10805. 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: arXiv administrators (email available below). General contact details of provider: http://arxiv.org/ .

    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.