Certified Symbolic Management of Financial Multi-party Contracts

Patrick Bahr, Jost Berthold, Martin Elsman

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer 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.
TitelICFP 2015 Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming
Antal sider13
UdgivelsesstedNew York, NY, USA
ForlagAssociation for Computing Machinery
Publikationsdato1 sep. 2015
ISBN (Trykt)978-1-4503-3669-7
StatusUdgivet - 1 sep. 2015


  • Certified Code, Coq, Domain-Specific Language, Financial Contracts, Haskell, Semantics, Type System


Dyk ned i forskningsemnerne om 'Certified Symbolic Management of Financial Multi-party Contracts'. Sammen danner de et unikt fingeraftryk.