论文标题
金融市场正式验证的交易
Formally Verified Trades in Financial Markets
论文作者
论文摘要
我们引入了一个正式的框架，用于分析金融市场的交易。如今，所有大型交易所都使用计算机算法来匹配买卖请求，这些算法必须遵守某些监管指南。例如，市场监管机构强迫交流产生的匹配应该是公平，统一和个人理性的。为了验证交易的这些属性，我们首先在定理供仪中正式定义这些概念，然后在匹配需求和供应方面开发许多重要的结果。最后，我们使用此框架来验证两种重要类拍卖机制的属性。本文中介绍的所有定义和结果均在COQ证明助手中完全正式化，而无需向其添加任何其他公理。
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.
