金融市场中形式化验证的交易
计算机科学中的逻辑
2020-07-22 v1 数据结构与算法
计算机科学与博弈论
交易与市场微观结构
摘要
我们引入一个用于分析金融市场中交易的形式化框架。如今，所有大型交易所都使用计算机算法来匹配买卖请求，且这些算法必须遵守特定的监管准则。例如，市场监管机构要求交易所产生的匹配应当是公平、一致且个体理性的。为验证交易的这些性质，我们首先在定理证明器中形式化定义这些概念，然后推导出关于供需匹配的许多重要结果。最后，我们利用该框架验证两类重要的双边拍卖机制的性质。本文给出的所有定义与结果均在Coq证明助手中完全形式化，且未向其添加任何额外公理。
引用
@article{arxiv.2007.10805,
title = {Formally Verified Trades in Financial Markets},
author = {Suneel Sarswat and Abhishek Kr Singh},
journal= {arXiv preprint arXiv:2007.10805},
year = {2020}
}
备注
Aceepted in ICFEM 2020. arXiv admin note: substantial text overlap with arXiv:1907.07885