准备，设置，验证！将hs-to-coq应用于实际的Haskell代码
Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code
摘要：
好的工具可以为用主流函数式语言编写的程序带来机械验证。我们使用hs-to-coq将Haskell容器库的重要部分转换为Coq，并根据我们从各种来源获得的规范进行验证，包括类型类定律，库的测试套件和Coq标准库的接口。我们的工作表明，它是可行的，以验证成熟的，广泛使用的，高度优化的，未经修改的Haskell代码。我们还学习了更多关于权重平衡树的理论，扩展了hs-to-coq来处理bug，并且--因为我们没有发现bug--证明了经过良好测试的功能代码的卓越质量。
英文摘要：
Good tools can bring mechanical verification to programs written in mainstream functional languages. We use hs-to-coq to translate significant portions of Haskell's containers library into Coq, and verify it against specifications that we derive from a variety of sources including type class laws, the library's test suite, and interfaces from Coq's standard library. Our work shows that it is feasible to verify mature, widely-used, highly optimized, and unmodified Haskell code. We also learn more about the theory of weight-balanced trees, extend hs-to-coq to handle partiality, and -- since we found no bugs -- attest to the superb quality of well-tested functional code.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
