Total Haskell是合理的
Total Haskell is Reasonable Coq
摘要：
我们想使用Coq证明助手来机械地验证Haskell程序的属性。为此，我们提出了一个工具，名为HS-to-Coq，总Haskell程序转换成Coq程序通过浅嵌入。我们应用我们的工具在三个案例研究-一个合法的单子实例，“赫顿剃刀”，和现有的数据结构库-并证明其正确性。这些例子表明，这种方法是可行的：既hs-to-coq适用于现有的Haskell代码，它产生的输出是经得起验证的。
英文摘要：
We would like to use the Coq proof assistant to mechanically verify properties of Haskell programs. To that end, we present a tool, named hs-to-coq, that translates total Haskell programs into Coq programs via a shallow embedding. We apply our tool in three case studies -- a lawful Monad instance, "Hutton's razor", and an existing data structure library -- and prove their correctness. These examples show that this approach is viable: both that hs-to-coq applies to existing Haskell code, and that the output it produces is amenable to verification.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
