Marlowe: financial contracts on Blockchain
summary
A small embedded Marlowe DSL in Haskell defines an executable small‑step semantics that runs as a single Plutus contract on a UTxO Cardano testbed; it includes built tooling: the Marlowe Playground visual/Blockly editor, simulator with stepwise execution, and SMT analysis (SBV → Z3) that finds issues like a missing payment, plus an Isabelle formalization with extracted Haskell checked by QuickCheck. Contracts add timeouts and commitments to avoid locked funds; ACTUS examples (including a guaranteed zero‑coupon bond) compile, simulate and analyze, while full on‑chain integration and tokenizable roles remain work in progress.
AI-written summary · about
chapters (41)
- 0:00Intro
- 3:17Haskell
- 3:34History of programming
- 4:38Highlevel languages
- 5:34Work as it were
- 6:19Working with a DSL
- 7:16Embedded DSL
- 8:25Financial DSL
- 8:57Financial Contract Example
- 11:15Constructs
- 11:58Conditions
- 12:13Legal system
- 12:54Limitation
- 13:50Contract operation
- 14:35Two sorts of correctness
- 15:13Interaction with the outside world
- 15:47Commitments
- 16:39Deposits
- 17:18Waiting
- 17:39Refund
- 18:00Commitment
- 18:41Language
- 20:07Actions
- 20:35Languages
- 22:56Interpreter
- 23:13User wallet
- 23:31Transactions
- 23:41Writing real contracts
- 25:29Financial Standard by Axis
- 25:56Zero Coupon Bond
- 26:53Self Enforcement
- 30:56Marlowe Playground
- 31:57Creating Contracts in a Visual Language
- 32:37Static Analysis
- 33:37Simulation
- 35:28Analysis
- 36:01Blocklis
- 37:34Live Demo
- 38:09Slideshow
- 38:28Backups
- 38:40SBV
related talks
45mFunctional Smart Contracts
45mPresent & Future of Blockchain Ⅱ
28mFrom Lambda to Ledger: An Architectural Comparison of Plinth and Plutarch
45mDeveloping DSLs with FP: Exploring 3 Strategies Through Examples
46mApplying Continuous Formal Methods to Cardano
29mPlinth: A Plugin-Powered Language Built on Haskell (Experience Report)
51mBuilding Distributed Applications in OCaml
01h 25mSpeculation in Smart Contracts