WIP：在Coq中正式制定Concordium共識協(xié)議
1月29日 · 1 分鐘閱讀
原作者：Thomas Dinsdale-Young，Bas Spitters，S?renEller Thomsen和Daniel Tschudi
我們報告了Coq的工業(yè)應用：我們?yōu)橐?guī)范Concordium區(qū)塊鏈共識協(xié)議所做的工作。這項工作目前處于NDA之下，但我們希望能夠在Coq正式發(fā)布前公布更多信息。最終，所有代碼都將在允許的開源許可下發(fā)布。這項工作是Concordium和Aarhus大學之間的合作。
?Concordium共識協(xié)議是一個可證安全的安全保證（POS）協(xié)議，在Haskell中有一個原型實現(xiàn)。 我們的目標是將crep-tographic安全證明與Haskell實現(xiàn)連接起來。 理想情況下，我們要么使用Coq的提取機制，要么使用hs-to-coq[?SB RW17]將形式化與Haskell實現(xiàn)連接起來。 我們的工作松散地基于Coq[PS18]中的Toychain形式化。Toychain是一種改進的類比特幣工作證明(PoW)協(xié)議。像toychain一樣，我們構建數(shù)學組件庫。
要獲取此科學論文的完整版本，請單擊此處。
快來發(fā)現(xiàn)Concordium并加入我們的社區(qū)！
開發(fā)人員中心：https：//development.concordium.com/tech
Gitter：https?:?//gitter.im/concordium_official/community
