A verifiable model of a minimal market operating sequentially, with price and time discrete

  • Dragiša Žunić The Institiute for Artificial Inteligence R&D of Serba
Keywords: formal logic, market design, financial exchanges, automated reasoning, logical frameworks, computational models


This research presents a minimal computational market model, i.e.,a model of a trading venue, with sequential order matching, in a declarative style, and proceeds to demonstrate how some fundamental properties can be formally proved. It is a challenging task to formally certify properties for a fundamental system in any realm of human endeavor, especially for systems with infinite state space. With the recent development of theoretical frameworks based on formal logic, it is now possible (albeit very difficult) to both formalize and reason about an object system in the same language. This research derives from the previous research presented in [1], and represents a simplification to obtain a minimal model. The computational model of a minimal market, presented here in a declarative style, is of importance from the perspective of both market design and verification.



Author Biography

Dragiša Žunić, The Institiute for Artificial Inteligence R&D of Serba




[1] I. Cervesato, S. Khan, G. Reis, and D. Žunić, “Formalization of automated trading systems in a concurrent linear framework,” In Proceeding of Linearity and TLLA, Oxford UK, 2019, pp. 1–15.

[2] E. Budish, P. Crampton, and J. Shim, “Implementation details for frequent batch auctions: slowing down markets to the blink of an eye,” American Economic Review Papers and Proceedings, Vol. 104, No. 5, pp. 418–424, 2014.

[3] E. Budish, P. Crampton, and J. Shim, “The high-frequency trading arms race: frequent batch auctions as a market design response,” Quarterly Journal of Economics, Vol. 130, No. 4, pp. 1547–1621, 2015.

[4] P. Bahr, J. Berthold, and M. Elsman, “Certified symbolic management of financial multi-party contracts,” In ICFP 2015, Vancouver, Canada, 2015, pp. 315–327.

[5] S. P. Jones, J. M. Eber, and J. Seward, “Composing Contracts: An Adventure in Financial Engineering (Functional Pearl),” In ICFP 2000, 2000, pp. 280–292.

[6] G. O. Passmore and D. Ignatovich, “Formal Verification of Financial Algorithms,” In CADE 26, Gothenburg, Sweden, 2017, pp. 26–41.

[7] D. Ignatovich and G. O. Passmore, Case Study: 2015 SEC Fine Against UBS ATS, Aesthetic Integration, Ltd., Technical Whitepaper, 2015.

[8] J. Y. Girard, “Linear Logic,” Theoretical Computer Science, Vol. 50, pp. 1–102, 1987.

[9] I. Cervesato, K. Watkins, F. Pfenning, and D. Walker, “A Concurrent Logical Framework I: Judgments and Properties,” Technical Report CMU-CS-02-101, CMU Pittsburgh, 2003.

[10] R. Harper, F. Honsell, and G. Plotkin, “A Framework for Defining Logics,” J. ACM, Vol. 50, pp. 143–184, 1993.