一句话：把 hs-to-coq 应用于 Haskell containers 库，验证其类型类定律与接口，并扩展 partiality 支持。
主流函数式语言程序缺乏机械化验证工具。本文使用 hs-to-coq 将 Haskell containers 库的重要部分翻译到 Coq，并依据类型类定律、库测试套件和 Coq 标准库接口等来源推导规约进行验证。结果表明，对成熟、广泛使用、高度优化且未修改的 Haskell 代码进行验证是可行的；作者还扩展 hs-to-coq 以处理 partiality，深化了对权重平衡树理论的理解，且未发现缺陷，佐证了经过良好测试的函数式代码的质量。
Abstract 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.
@article{paperbot1227,
title = {Ready,
<tt>Set</tt>
, Verify! Applying
<tt>hs-to-coq</tt>
to real-world Haskell code},
author = {JOACHIM BREITNER and ANTAL SPECTOR-ZABUSKY and YAO LI and CHRISTINE RIZKALLAH and JOHN WIEGLEY and JOSHUA COHEN and STEPHANIE WEIRICH},
journal = {Journal of Functional Programming},
volume = {31},
year = {2021},
doi = {10.1017/s0956796820000283}
}