Haskell程序到Agda的转换及其推理方法
An approach to translating Haskell programs to Agda and reasoning about them
摘要：
我们使用Agda程序设计语言和证明助手来正式验证基于HotStuff / LibraBFT的拜占庭容错共识实现的正确性。Agda实现是我们基于LibraBFT的Haskell实现的翻译。这篇简短的论文集中在这项工作的一个方面。我们开发了一个库，使翻译后的Agda实现能够紧密地反映它所基于的Haskell代码。这使得更容易和更有效地审查翻译的准确性，并在Haskell代码更改时维护翻译的Agda代码，从而降低翻译错误的风险。我们还解释了我们如何捕捉我们的库提供的语法功能的语义，从而使正式的推理程序使用它们，我们如何推理所产生的Agda实现的细节将在未来的论文。我们提供的库独立于我们的特定验证项目，并且是开源的，可供其他人使用和扩展。
英文摘要：
We are using the Agda programming language and proof assistant to formally verify the correctness of a Byzantine Fault Tolerant consensus implementation based on HotStuff / LibraBFT. The Agda implementation is a translation of our Haskell implementation based on LibraBFT. This short paper focuses on one aspect of this work. We have developed a library that enables the translated Agda implementation to closely mirror the Haskell code on which it is based. This makes it easier and more efficient to review the translation for accuracy, and to maintain the translated Agda code when the Haskell code changes, thereby reducing the risk of translation errors. We also explain how we capture the semantics of the syntactic features provided by our library, thus enabling formal reasoning about programs that use them; details of how we reason about the resulting Agda implementation will be presented in a future paper. The library that we present is independent of our particular verification project, and is available, open-source, for others to use and extend.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
