Prototype implementation of domain-specific language for the design of smart-contracts over cryptocurrencies
Branch: master
Clone or download
Type Name Latest commit message Commit time
Failed to load latest commit information.
coq Fix problem with newline encoding in Makefile Oct 24, 2018
extraction_test Add property for comparing extracted and original semantics Oct 29, 2018
meadow Make export to Meadow clear workspace Dec 18, 2018
new-semantics Isabelle formalisation and termination proof of new semantics Feb 15, 2019
presentations Added ISoLA presentation (PDF and Keynote). Nov 8, 2018
src Refactor EscrowV2.hs Dec 5, 2018
tex Added author proof Oct 16, 2018
.gitignore Use Marlowe.Observation to represent SPJ Observables. This allows to … Sep 28, 2018
LICENSE Update License Feb 13, 2019
marlowe.cabal Add basic tests Oct 12, 2018


This repository contains the design of Marlowe, a DSL for describing smart-contracts that can be enforced by scripts deployed on a cryptocurrency's blockchain, and some tools for analysing and simulating the execution of contracts written in the DSL. The following are some of the main files included in this repository:

  • src/Semantics.hs — contains the small-step semantics of DSL (stepBlock function), together with a simple driver (driver function).
  • src/ContractFormatter.hs — contains the implementation of a formatter for scdsl code.
  • src/SmartInputs.hs — contains code that calculates possible inputs for a given input, state, contract, and observables value.
  • src/DepositIncentive.hs — contains an example contract for incentivising saving.
  • src/CrowdFunding.hs — contains an example contract for crowd-funding limited to 4 participants.
  • src/Escrow.hs — contains an example contract for an escrow payment.

A full description of the v1.3 version was presented at ISoLA 2018, and the paper is available here.


Meadow is a browser-based demo prototype that supports graphical editing of smart-contracts (thanks to the Blockly library) and block by block simulation of their execution (translated from the semantics thanks to the Haste compiler).

Meadow is available at: and a video showing Meadow in Action is here:

The sources for Meadow are available in the meadow folder.

Build on MacOS

Requirements: Homebrew, Haskell Stack 1.6 or later.

Install Haskell Stack if you haven't already

$ brew install haskell-stack

$ brew install glpk
$ stack setup
$ stack build

Stable branch

The master branch contains the latest developments of Marlowe, because of this, the Haskell semantics, the Coq formalisation, and the Meadow imlementation may be out of sync with each other in this branch. The stable branch marks a previous version of Marlowe where the different components are in sync.