一句话：将 Haskell containers 库翻译到 Coq 并验证，证明可验证成熟、未修改的函数式代码。
本文是一篇经验报告，探讨能否对主流函数式语言编写的成熟代码进行机械验证。作者使用 hs-to-coq 将 Haskell 的 containers 库中相当一部分代码翻译到 Coq，并依据来自类型类定律、库测试套件以及 Coq 标准库接口等多种来源的规约进行验证。结果表明，验证成熟、广泛使用、高度优化且未经修改的 Haskell 代码是可行的。作者还深化了对权重平衡树理论的理解，扩展 hs-to-coq 以处理 partiality，并且由于未发现 bug，侧面印证了经过充分测试的函数式代码具有极高质量。
Good tools can bring mechanical verification to programs written in mainstream functional languages. We use <pre>hs-to-coq</pre> to translate significant portions of Haskell’s <pre>containers</pre> 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 <pre>hs-to-coq</pre> to handle partiality, and – since we found no bugs – attest to the superb quality of well-tested functional code.
@article{paperbot294,
title = {Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report)},
author = {Joachim Breitner and Antal Spector-Zabusky and Yao Li and Christine Rizkallah and John Wiegley and Stephanie Weirich},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
number = {ICFP},
year = {2018},
doi = {10.1145/3236784}
}