A calculus for Bitcoin smart contracts

Besides simple transfers of currency, Bitcoin also enables various forms of smart contracts, i.e. protocols where users interact within pre-agreed rules, which determine (possibly depending on the actual interaction) how currency is eventually distributed. We provide a gentle introduction to Bitcoin smart contracts, which we specify by abstracting from the underlying Bitcoin machinery. To this purpose we exploit BitML, a recent DSL for smart contracts executable on Bitcoin.