原作者：来自Aarhus大学的Danil Annenkov和Bas Spitters
（这项工作得到丹麦奥尔胡斯大学Concordium区块链研究中心的支持，并于2019年出版）
我们提出了一种使用元编程技术将功能性智能合约语言嵌入Coq证明助手的新颖方法。
我们的框架允许使用深度嵌入来开发智能合约语言的元理论，并为使用浅层嵌入来推理具体合约提供了一种方便的方法。
所提出的方法允许将两个嵌入项以稳健定理的形式连接起来。作为我们方法的一个实例，我们在Coq中嵌入了Oak智能合约语言，并验证了众筹合约的几个重要特性。
所开发的技术适用于所有功能性智能合约语言。
要获取此科学论文的完整版本，请单击此处。
快来发现Concordium并加入我们的社区！
开发人员中心：https：//development.concordium.com/tech
Gitter：https : //gitter.im/concordium_official/community
