Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code

Joachim Breitner, Antal Spector-Zabusky, Yao Li +3

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 libr…