Double sided auctions are widely used in financial markets to match demand and supply . We extend notions of double sided auctions to incorporate multiple quantity trade requests . We establish new uniqueness theorems that enable automatic detection ofviolations in an exchange program by comparing its output with that of averified program . We extract verified OCaml and Haskell programsthat can be used by the exchanges and the regulators of the financial markets. We demonstrate the practical applicability of our work by running the verifiedprogram on real market data from an exchange to automatically check for violations in the exchange algorithm . All proofs are formalized in the Coq proof assistant without adding any axiom to the system .

Author(s) : Raja Natarajan, Suneel Sarswat, Abhishek Kr Singh

Links : PDF - Abstract

Code :

Keywords : double - sided - auctions - exchange - financial -

Leave a Reply

Your email address will not be published. Required fields are marked *