@InProceedings{contracts,
  Title = {Certified Symbolic Management of Financial Multi-party Contracts},
  Author = {Bahr, Patrick and Berthold, Jost and Elsman, Martin},
  Booktitle = {Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming},
  Year = {2015},
  Address = {New York, NY, USA},
  Month = aug,
  Date = {2015-08-29},
  Pages = {315--327},
  Publisher = {ACM},
  Series = {ICFP 2015},
  Abstract = {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.},
  Acmid = {2784747},
  Doi = {10.1145/2784731.2784747},
  ISBN = {978-1-4503-3669-7},
  Keywords = {Certified Code, Rocq, Domain-Specific Language, Financial Contracts, Haskell, Semantics, Type System},
  Location = {Vancouver, BC, Canada},
  Numpages = {13},
  Url = {http://doi.acm.org/10.1145/2784731.2784747}
}