金融市场中交易的正式验证

我们引入一个用于分析金融市场中交易的正式框架。交易所是多个买方和卖方参与交易的地方。如今，所有大型交易所都使用实现双边拍卖的计算机算法来匹配买卖请求，且这些算法必须遵守某些监管准则。例如，市场监管机构要求交易所产生的匹配应当是公平、统一和个体理性的。为验证这些交易属性，我们首先在定理证明器中正式定义这些概念，然后给出关于匹配的相关结果的正式证明。最后，我们利用该框架验证两类重要双边拍卖的属性。本文给出的所有定义和结果均在Coq证明助手中完全形式化，未添加任何额外公理。