论文标题
阿尔伯特（Albert），Tezos区块链的中级智能合同语言
Albert, an intermediate smart-contract language for the Tezos blockchain
论文作者
论文摘要
Tezos是一个智能合同区块链。 Tezos智能合约用一种名为Michelson的低级堆栈语言编写。在本文中，我们介绍了Albert，这是一种用于Tezos Smart合同的中级语言，该语言将Michelson堆叠为线性键入记录。我们还描述了用Coq撰写的米歇尔森的编译器，该编译器针对Mi-Cho-Coq，这是COQ中实施的Michelson的正式规范。
Tezos is a smart-contract blockchain. Tezos smart contracts are written in a low-level stack-based language called Michelson. In this article we present Albert, an intermediate language for Tezos smart contracts which abstracts Michelson stacks as linearly typed records. We also describe its compiler to Michelson, written in Coq, that targets Mi-Cho-Coq, a formal specification of Michelson implemented in Coq.
