2017/11/25 by Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah +1 · 1 voice · 1 citation
Computer Science · #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.PL
paper · pdf · doi:10.1145/3167092
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
arxiv created 2017/11/25 · arxiv published 2017/11/25 · arxiv updated 2017/11/28 · openalex created_date 2017/12/04 · openalex publication_date 2018/01/08 · openalex updated_date 2026/08/01
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.