一种将 Haskell 程序翻译为 Agda 并进行推理的方法
计算机科学中的逻辑
2022-05-19 v1 编程语言
软件工程
摘要
我们使用 Agda 编程语言和证明助手来形式化验证基于 HotStuff / LibraBFT 的拜占庭容错共识实现的正确性。该 Agda 实现是基于 LibraBFT 的 Haskell 实现的翻译。本短文聚焦于这项工作的一个方面。我们开发了一个库，使翻译后的 Agda 实现能够紧密镜像其所基于的 Haskell 代码。这使得审查翻译的准确性更加容易和高效，并在 Haskell 代码变更时维护翻译后的 Agda 代码，从而降低翻译错误的风险。我们还解释了如何捕获我们库所提供的语法特征的语义，从而能够对使用这些特征的程序进行形式化推理；关于我们如何对所得 Agda 实现进行推理的细节将在未来的论文中介绍。我们提出的库独立于我们特定的验证项目，并且作为开源可供他人使用和扩展。
引用
@article{arxiv.2205.08718,
title = {An approach to translating Haskell programs to Agda and reasoning about them},
author = {Harold Carr and Christa Jenkins and Mark Moir and Victor Cacciari Miraldo and Lisandra Silva},
journal= {arXiv preprint arXiv:2205.08718},
year = {2022}
}