Pacta sunt servanda: Legal contracts in Stipula

We present Stipula, a domain specific language that may assist legal practitioners in programming legal contracts through specific patterns. The language is based on a small set of programming abstractions that correspond to common patterns in legal contracts. We illustrate the language by means of two paradigmatic legal contracts: a bike rental and a bet contract. Stipula comes with a formal semantics, an observational equivalence and a type inference system, that provide for a clear account of the contracts' behaviour and illustrate how several concepts from concurrency theory can be adapted to automatically verify the properties and the correctness of software-based legal contracts. We also discuss a prototype centralized implementation of Stipula.