A Typed Programmatic Interface to Contracts on the Blockchain
summary
Defines a concrete, type-safe interaction between OCaml programs and Tezos contracts and proves preservation and progress for that execution model. Provides a runtime-checked cast from public hash to a typed contract that issues an RPC query to verify parameter and storage shapes, and models non‑blocking originate/transfer returning an operation hash plus a blocking cast to a contract handle. Ships as an OCaml prototype for Tezos and includes a worked counter example and formal meta‑theory.
AI-written summary · about
chapters (13)
- 0:00Intro
- 0:20Context
- 2:11Interoperation with contracts
- 2:58Use cases for interoperation
- 3:41This work
- 4:39Out of the box
- 5:48Example contract: A counter in Michelson
- 7:12API: Preparation
- 8:25Automatizing the contract - keep counter close to target
- 10:15Execution model
- 11:33Type system
- 13:46Typing rules!
- 14:40Conclusions
related talks
45mFunctional Smart Contracts
12mNative atomic composability
45mMarlowe: financial contracts on Blockchain
31mPrivacy-preserving smart contracts
30m5 Reasons Why Tezos Rocks
05mTezDev Paris 2022 - Jordan Vertaure
06mTezos x WeAreDevs World Congress 2022 - Poorvi Sachar
32mSoK: Private Programmability on Blockchain Systems