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}
}