用Coq增强Tezos智能合约的可靠性
编程语言
2021-06-25 v1
摘要
Tezos是一个智能合约区块链。Tezos智能合约用一种称为Michelson的底层基于栈的语言编写。本文概述了使用Coq证明辅助器对Michelson智能合约获得更强保证的努力：Mi-Cho-Coq框架，一个定义Michelson形式语义的Coq库，以及一个解释器、一个简单的优化器和用于推理Michelson智能合约的最弱前置条件演算；Albert，一种用栈抽象Michelson的中间语言，带有以Mi-Cho-Coq为目标、用Coq编写的编译器。
引用
@article{arxiv.2106.12973,
title = {Making Tezos smart contracts more reliable with Coq},
author = {Bruno Bernardo and Raphaël Cauderlier and Guillaume Claret and Arvid Jakobsson and Basile Pesin and Julien Tesson},
journal= {arXiv preprint arXiv:2106.12973},
year = {2021}
}