Formal modelling of smart contract languages and introduction to BitML

22^nd April 2021, 14:00
Alexei Lisitsa
University of Liverpool

Abstract

Smart Contracts have become very popular recently. In this talk, I will address the questions of formal modelling of smart contracts languages and their expressive power ("what kind of contracts can be/cannot be expressed"). As the main modelling formalism, I will introduce BitML, a high-level and declarative formal language proposed recently by M. Bartoletti and R. Zunino for Bitcoin contracts specification. I will present some results and open questions on the expressive power of BitML and its extensions.