经认证的金融合同汇编
Certified Compilation of Financial Contracts
摘要：
我们提出了一个扩展认证的金融合同管理系统，允许模板化的声明性金融合同，并通过验证编译成所谓的支付表达式与金融随机模型集成。这样的表达式很容易允许在给定的评估上下文中确定合同的价值，例如为随机模拟创建的上下文。模板机制在契约规范级别非常有用，用于编写通用的可重用契约，以及重用代码，如果没有模板机制，需要重新编译以用于不同的评估上下文。我们报告的效果，使用认证系统的背景下，基于GPGPU的蒙特卡罗模拟引擎定价各种场外（OTC）金融合约。完整的合同管理系统，包括支付语言编译，在Coq证明助手中进行了验证，并且从我们的Coq开发中提取了经过认证的Haskell代码以及Futhark代码，用于数据并行定价引擎。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
