Total Haskell is Reasonable Coq
Programming Languages
2017-11-28 v1
Abstract
We would like to use the Coq proof assistant to mechanically verify properties of Haskell programs. To that end, we present a tool, named hs-to-coq, that translates total Haskell programs into Coq programs via a shallow embedding. We apply our tool in three case studies -- a lawful Monad instance, "Hutton's razor", and an existing data structure library -- and prove their correctness. These examples show that this approach is viable: both that hs-to-coq applies to existing Haskell code, and that the output it produces is amenable to verification.
Cite
@article{arxiv.1711.09286,
title = {Total Haskell is Reasonable Coq},
author = {Antal Spector-Zabusky and Joachim Breitner and Christine Rizkallah and Stephanie Weirich},
journal= {arXiv preprint arXiv:1711.09286},
year = {2017}
}
Comments
13 pages plus references. Published at CPP'18, In Proceedings of 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP'18). ACM, New York, NY, USA, 2018