Certified Symbolic Management of Financial Multi-party Contracts

Patrick Bahr, Jost Berthold, Martin Elsman

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review


Domain-specific languages (DSLs) for complex financial contracts are in practical use in many banks and financial institutions today. Given the level of automation and pervasiveness of software in the sector, the financial domain is immensely sensitive to software bugs. At the same time, there is an increasing need to analyse (and report on) the interaction between multiple parties. In this paper, we present a multi-party contract language that rigorously relegates any artefacts of simulation and computation from its core, which leads to favourable algebraic properties, and therefore allows for formalising domain-specific analyses and transformations using a proof assistant. At the centre of our formalisation is a simple denotational semantics independent of any stochastic aspects. Based on this semantics, we devise certified contract analyses and transformations. In particular, we give a type system, with an accompanying type inference procedure, that statically ensures that contracts follow the principle of causality. Moreover, we devise a reduction semantics that allows us to evolve contracts over time, in accordance with the denotational semantics. From the verified Coq definitions, we automatically extract a Haskell implementation of an embedded contract DSL along with the formally verified contract management functionality. This approach opens a road map towards more reliable contract management software, including the possibility of analysing contracts based on symbolic instead of numeric methods.
Original languageEnglish
Title of host publicationICFP 2015 Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming
Number of pages13
Place of PublicationNew York, NY, USA
PublisherAssociation for Computing Machinery
Publication date1 Sept 2015
ISBN (Print)978-1-4503-3669-7
Publication statusPublished - 1 Sept 2015


Dive into the research topics of 'Certified Symbolic Management of Financial Multi-party Contracts'. Together they form a unique fingerprint.

Cite this