面向金融市场的已验证双边拍卖

双边拍卖在金融市场中被广泛用于匹配供需。已有关于双边拍卖的研究主要集中于单一数量交易请求。我们将双边拍卖的多种概念扩展至包含多数量交易请求的情形，并提供完全形式化的双边拍卖匹配算法及其正确性证明。我们建立了新的唯一性定理，能够通过将某交易程序的输出与已验证程序的输出进行比较，自动检测该程序中的违规。所有证明均在 Coq 证明助手中形式化，未向系统添加任何公理。我们提取了可供金融市场交易所与监管机构使用的已验证 OCaml 与 Haskell 程序。我们通过将已验证程序运行于某交易所的真实市场数据，自动检查其交易算法中的违规，从而展示了本工作的实际适用性。