We present an extension to a certified financial contract management system that allows for templated declarative financial contracts and for integration with financial stochastic models through verified compilation into so-called payoff-expressions. Such expressions readily allow for determining the value of a contract in a given evaluation context, such as contexts created for stochastic simulations. The templating mechanism is useful both at the contract specification level, for writing generic reusable contracts, and for reuse of code that, without the templating mechanism, needs to be recompiled for different evaluation contexts. We report on the effect of using the certified system in the context of a GPGPU-based Monte Carlo simulation engine for pricing various over-the-counter (OTC) financial contracts. The full contract-management system, including the payoff-language compilation, is verified in the Coq proof assistant and certified Haskell code is extracted from our Coq development along with Futhark code for use in a data-parallel pricing engine.
翻译:我们提出一个经认证的金融合同管理系统的扩展,允许将申报性金融合同模板和通过经过核查的汇编而与金融随机模型相结合,将其纳入所谓的 " 报酬表度 " 中,这种表达方式很容易确定合同在特定评价背景下的价值,例如为随机模拟创造的环境。在合同规格、编写通用可重复使用合同和重新使用没有临时机制需要重新编译的不同评价背景下的代码方面,采用经认证的系统对基于GPGPPPPU的蒙特卡洛模拟引擎为各种超计费用财务合同定价的效果提出报告。完整的合同管理系统,包括支付性语言汇编,在Coq验证助理中进行验证,从我们的Coq开发中提取经认证的Haskell代码,以及用于数据平行定价引擎的Futhark代码。