论文标题
将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.
