A verifiable model of a minimal market operating sequentially, with price and time discrete
Abstract
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.
References
[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.
I (we), the author(s), hereby declare under full moral, financial and criminal liability that the manuscript submitted for publication to the Journal of Computer and Forensic Sciences
a) is the result of my (our) own original research and that I (we) hold the right to publish it;
b) does not infringe any copyright or other third-party proprietary rights;
c) complies with the Journal’s research and publishing ethics standards;
d) has not been published elsewhere, under this or any other title;
e) is not under consideration by another publication, under this or any other title.
I (we) also declare under full moral, financial and criminal liability:
f) that all conflicts of interest that may directly or potentially influence or impart bias on the work have been disclosed in the manuscript;
g) that if the article has been accepted for publishing I (we) will transfer all copyright ownership of the manuscript to the University of Criminal Investigation and Police Studies in Belgrade.
Signed by the Corresponding Author on behalf of the all other authors.