WIP：在Coq中正式制定Concordium共识协议
1月29日 · 1 分钟阅读
原作者：Thomas Dinsdale-Young，Bas Spitters，SørenEller Thomsen和Daniel Tschudi
我们报告了Coq的工业应用：我们为规范Concordium区块链共识协议所做的工作。这项工作目前处于NDA之下，但我们希望能够在Coq正式发布前公布更多信息。最终，所有代码都将在允许的开源许可下发布。这项工作是Concordium和Aarhus大学之间的合作。
Concordium共识协议是一个可证安全的安全保证（POS）协议，在Haskell中有一个原型实现。 我们的目标是将crep-tographic安全证明与Haskell实现连接起来。 理想情况下，我们要么使用Coq的提取机制，要么使用hs-to-coq[ SB RW17]将形式化与Haskell实现连接起来。 我们的工作松散地基于Coq[PS18]中的Toychain形式化。Toychain是一种改进的类比特币工作证明(PoW)协议。像toychain一样，我们构建数学组件库。
要获取此科学论文的完整版本，请单击此处。
快来发现Concordium并加入我们的社区！
开发人员中心：https：//development.concordium.com/tech
Gitter：https : //gitter.im/concordium_official/community
