License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.FMBC.2021.5
URN: urn:nbn:de:0030-drops-154294
Go to the corresponding OASIcs Volume Portal

Doan, Thi Thu Ha ; Thiemann, Peter

Towards Contract Modules for the Tezos Blockchain (Short Paper)

OASIcs-FMBC-2021-5.pdf (0.5 MB)


Programmatic interaction with a blockchain is often clumsy. Many interfaces handle only loosely structured data, often in JSON format, that is inconvenient to handle and offers few guarantees.
Contract modules provide a statically checked interface to interact with contracts on the Tezos blockchain. A module specification provides all types as well as information about potential failure conditions of the contract. The specification is checked against the contract implementation using symbolic execution. An OCaml module is generated that contains a function for each entry point of the contract. The types of these functions fully describe the interface including the failure conditions and guarantee type-safe and sometimes fail-safe invocation of the contract on the blockchain.

BibTeX - Entry

  author =	{Doan, Thi Thu Ha and Thiemann, Peter},
  title =	{{Towards Contract Modules for the Tezos Blockchain}},
  booktitle =	{3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)},
  pages =	{5:1--5:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-209-9},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{95},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-154294},
  doi =		{10.4230/OASIcs.FMBC.2021.5},
  annote =	{Keywords: contract API, modules, static checking}

Keywords: contract API, modules, static checking
Collection: 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)
Issue Date: 2021
Date of publication: 30.11.2021
Supplementary Material: Software (Source Code):

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI