Formally Verified Trades in Financial Markets

Suneel Sarswat and Abhishek Kr Singh

Papers from arXiv.org

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.

Date: 2020-07
References: View references in EconPapers View complete reference list from CitEc
Citations:

Downloads: (external link)
http://arxiv.org/pdf/2007.10805 Latest version (application/pdf)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:arx:papers:2007.10805

Access Statistics for this paper

More papers in Papers from arXiv.org
Bibliographic data for series maintained by arXiv administrators ().