Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code
Programming Languages
2018-03-21 v2
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.
Keywords
Cite
@article{arxiv.1803.06960,
title = {Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code},
author = {Joachim Breitner and Antal Spector-Zabusky and Yao Li and Christine Rizkallah and John Wiegley and Stephanie Weirich},
journal= {arXiv preprint arXiv:1803.06960},
year = {2018}
}
Comments
30 pages, submitted to ICFP'18