Marlowe: Financial Contracts on Blockchain
Blockchains allow the specification of contracts in the form of programs that guarantee their fulfilment. Nevertheless, errors in those programs can cause important, and often irretrievable, monetary loss. General-purpose languages provide a platform on w
- PDF / 11,179,841 Bytes
- 20 Pages / 439.37 x 666.142 pts Page_size
- 94 Downloads / 234 Views
and Simon Thompson(B)
School of Computing, University of Kent, Canterbury, UK {p.lamela-seijas,s.j.thompson}@kent.ac.uk
Abstract. Blockchains allow the specification of contracts in the form of programs that guarantee their fulfilment. Nevertheless, errors in those programs can cause important, and often irretrievable, monetary loss. General-purpose languages provide a platform on which contracts can be built, but by their very generality they have the potential to exhibit behaviours of an unpredictable kind, and are also not easy to read or comprehend for general users. An alternative solution is provided by domain-specific languages (DSLs), which are designed to express programs in a particular field. This paper explores the design of one DSL, Marlowe, targeted at the execution of financial contracts in the style of Peyton Jones et al. on blockchains. We present an executable semantics of Marlowe in Haskell, an example of Marlowe in practice, and describe the Meadow tool that allows users to interact in-browser with simulations of Marlowe contracts.
1
Introduction
This paper explores the design of a domain specific language, Marlowe,1,2 targeted at the execution of financial contracts in the style of Peyton Jones, Eber and Seward [16] on blockchains. In doing this, we are required to refine the model of contracts in a number of ways in order to fit with a radically different context. Consider the following example of an “escrow” contract so that we can explain the motivation more concretely. The aim of this contract, written in functional pseudocode in the style of [16] involves three participants: alice , bob and carol . alice is to pay an amount of money to bob on receipt of goods from her. alice pays the money into escrow controlled by carol . There are two options for the money: if two out of the three participants agree to pay it to bob , that goes ahead; if, on the other hand, two of the participants opt to refund the money to alice , that is done instead. This work is part of the Cardano project and is supported by IOHK, https://iohk.io. 1 Named after Christopher Marlowe, the Elizabethan poet, dramatist and spy, who was born and educated in Canterbury, en.wikipedia.org/wiki/Christopher Marlowe. 2 Marlowe is available from https://github.com/input-output-hk/scdsl. c Springer Nature Switzerland AG 2018 T. Margaria and B. Steffen (Eds.): ISoLA 2018, LNCS 11247, pp. 356–375, 2018. https://doi.org/10.1007/978-3-030-03427-6_27
Marlowe: Financial Contracts on Blockchain
357
The outer primitive When waits until the condition – its first argument – becomes true; in this case, the condition is that either two participants choose refund or two participants choose pay . The second argument of the When is itself another Contract, which is performed after the condition of the When has been met, and it makes the payment if two participants chose pay , otherwise it redeems previous money commitments. (When (Or (two_chose alice bob carol refund) (two_chose alice bob carol pay)) (Choice (two_chose alice bob carol pay) (
Data Loading...
