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
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/15429/
Doan, Thi Thu Ha ;
Thiemann, Peter
Towards Contract Modules for the Tezos Blockchain (Short Paper)
Abstract
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
@InProceedings{doan_et_al:OASIcs.FMBC.2021.5,
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 = {https://drops.dagstuhl.de/opus/volltexte/2021/15429},
URN = {urn:nbn:de:0030-drops-154294},
doi = {10.4230/OASIcs.FMBC.2021.5},
annote = {Keywords: contract API, modules, static checking}
}
