Verifying haskell programs using constructive type theory
Verifying haskell programs using constructive type theory
复制标题
使用构造类型理论验证 haskell 程序
DOI：
10.1145/1088348.1088355
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
U. Norell
中科院分区：
文献类型：
--
作者：
Andreas Abel;Marcin Benke;Ana Bove;John Hughes;U. Norell
基于依赖类型理论的证明助手与函数式编程语言密切相关，因此很容易使用它们来证明函数式程序的正确性。在本文中，我们展示了如何使用 Agda 这样的证明助手来证明 Haskell 程序的定理。 Haskell 程序被翻译成其语义的 Agda 模型，通过 GHC 的核心语言翻译成特别适合在 Agda 谓词类型系统中表示 Haskell 多态性的一元形式。通过适当地实例化 monad，翻译可以支持仅对总值或总值和部分值进行推理。我们声称，虽然这些 Agda 模型是通过相对复杂的翻译过程生成的，但它们的证明是简单自然的，并且我们提供了许多例子来支持这一说法。
Proof assistants based on dependent type theory are closely related to functional programming languages, and so it is tempting to use them to prove the correctness of functional programs. In this paper, we show how Agda, such a proof assistant, can be used to prove theorems about Haskell programs. Haskell programs are translated into an Agda model of their semantics, by translating via GHC's Core language into a monadic form specially adapted to represent Haskell's polymorphism in Agda's predicative type system. The translation can support reasoning about either total values only, or total and partial values, by instantiating the monad appropriately. We claim that, although these Agda models are generated by a relatively complex translation process, proofs about them are simple and natural, and we offer a number of examples to support this claim.