A Typed Programmatic Interface to Contracts on the Blockchain
arXiv:2108.11867
Abstract
Smart contract applications on the blockchain can only reach their full potential if they integrate seamlessly with traditional software systems via a programmatic interface. This interface should provide for originating and invoking contracts as well as observing the state of the blockchain. We propose a typed API for this purpose and establish some properties of the combined system. Specifically, we provide an execution model that enables us to prove type-safe interaction between programs and the blockchain. We establish further properties of the model that give rise to requirements on the API. A prototype of the interface is implemented in OCaml for the Tezos blockchain.
19 pages + 8 pages appendix. Appears in APLAS 2021. Extended version with proofs in appendix