The Design of a Practical Proof Checker for a Lazy Functional Language

Pure, lazy functional languages like Haskell provide a sound basis for formal reasoning about programs in an equational style. In practice, however, equational reasoning is underutilized. We suggest that part of the reason for this is the lack of accessible tools for developing machine-checked equational reasoning proofs. This paper outlines the design of MProver, a system which fills just that niche. MProver features first-class support for reasoning about potentially undefined computations (particularly important in a lazy setting), and an extended notion of Haskell-like type classes, enabling a highly modular style of program verification that closely follows familiar functional programming idioms.