双向拍卖：形式化与自动化检查器
Double Auctions: Formalization and Automated Checkers
AI总结：
本文将双向拍卖匹配算法扩展到多数量请求，在 Coq 中完成形式化与正确性证明，并抽取 OCaml/Haskell 程序用于自动检查交易所算法违规。
摘要：
双向拍卖被广泛用于股票、衍生品、货币和商品等金融市场，以匹配需求与供给。当所有买方和卖方都提交交易请求后，交易所决定这些请求应如何匹配。决定匹配的两个最常见目标，是以统一价格最大化交易量，以及通过动态定价最大化交易量。先前研究主要集中于单一数量的交易请求。在本工作中，我们扩展该框架以处理多数量交易请求，并给出双向拍卖的完全形式化匹配算法及其正确性证明。我们建立了新的唯一性定理，从而能够通过将交易所系统的输出与经验证程序的输出进行比较，自动检测交易所系统中的违规行为。所有证明均在 Coq Proof Assistant 中形式化，并且我们抽取了经验证的 OCaml 和 Haskell 程序，这些程序可作为交易所和市场监管机构的资源。通过在来自某交易所的真实市场数据上运行该经验证程序，以自动检查交易所算法中的违规行为，我们展示了本工作的实际适用性。
英文摘要：
Double auctions are widely used in financial markets, such as those for stocks, derivatives, currencies, and commodities, to match demand and supply. Once all buyers and sellers have placed their trade requests, the exchange determines how these requests are to be matched. The two most common objectives for determining the matching are maximizing trade volume at a uniform price and maximizing trade volume through dynamic pricing. Prior research has primarily focused on single-quantity trade requests. In this work, we extend the framework to handle multiple-quantity trade requests and present fully formalized matching algorithms for double auctions, along with their correctness proofs. We establish new uniqueness theorems, enabling automatic detection of violations in exchange systems by comparing their output to that of a verified program. All proofs are formalized in the Coq Proof Assistant, and we extract verified OCaml and Haskell programs that could serve as a resource for exchanges and market regulators. We demonstrate the practical applicability of our work by running the verified program on real market data from an exchange to automatically check for violations in the exchange algorithm.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
