Total Haskell is Reasonable Coq

TL;DR

This paper introduces hs-to-coq, a tool that translates total Haskell programs into Coq for formal verification, demonstrating its effectiveness through case studies on various Haskell codebases.

Contribution

The paper presents a novel tool, hs-to-coq, enabling the verification of Haskell programs within Coq, bridging the gap between Haskell code and formal proof environments.

Findings

hs-to-coq successfully translates real Haskell code into Coq.

The translated code is suitable for formal verification in Coq.

Case studies verify the correctness of Haskell programs using hs-to-coq.

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.