Certified Compilation of Financial Contracts

Danil Annenkov, Martin Elsman

    3 Citations (Scopus)

    Abstract

    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.

    Original languageUndefined/Unknown
    Title of host publicationProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming
    Place of PublicationNew York, NY, USA
    PublisherAssociation for Computing Machinery
    Publication date3 Sept 2018
    Pages5:1-5:13
    ISBN (Print)978-1-4503-6441-6
    DOIs
    Publication statusPublished - 3 Sept 2018
    Event20th International Symposium on Principles and Practice of Declarative Programming : PPDP 2018 - Frankfurt am Main, Germany
    Duration: 3 Sept 20185 Sept 2018

    Conference

    Conference20th International Symposium on Principles and Practice of Declarative Programming
    Country/TerritoryGermany
    CityFrankfurt am Main
    Period03/09/201805/09/2018

    Cite this