Banks and financial institutions nowadays often use domain-specific languages (DSLs) for describing complex financial contracts, in particular, for specifying how asset transfers for a specific contract depend on underlying observables, such as interest rates, currency rates, and stock prices. The seminal work by Peyton-Jones and Eber on financial contracts shows how an algebraic approach to contract specification can be used for valuation of contracts (when combined with a model of the underlying observables) and for managing how contracts evolve under so-called fixings and decision-taking, with the contracts eventually evaporating into the empty contract, for which no party have further obligations. The ideas have emerged into Eber's company LexiFi, which has become a leading software provider for a range of financial institutions, with all contract management operations centralised around a domain-specific contract language hosted in MLFi, a derivative of the functional programming language OCaml. In this paper, we present a small simple contract language, which rigorously relegates any artefacts of modelling and computation from its core. The language shares the same vision as the previously mentioned work with the addition that it (a) allows for specifying multi-party contracts (such as entire portfolios), (b) has good algebraic properties, well suited for formal reasoning, and yet (c) allows for expressing many interesting contracts appearing in real-world portfolios, such as various variations of so-called barrier options. We show that plenty of information can be derived from, and useful manipulations defined on, just the symbolic contract specification, independent of any stochastic aspects of the modelled contracts. Contracts modelled in our language are analysed and transformed for management according to a precise cash-flow semantics, modelled and checked using the Coq proof assistant. Implementations of the contract language in Haskell and Coq are available online together with machine-checkable proofs (in Coq) of the key properties of the contract language.
|Titel||Proceedings of the 26th Nordic Workshop on Programming Theory, NWPT '14|
|Publikationsdato||1 okt. 2014|
|Status||Udgivet - 1 okt. 2014|
- financial contracts, multi-party contracts, formal verification, Haskell, Coq