Implementation of a Pragmatic Translation from Haskell into Isabelle/HOL

Abstract

Among other things the functional programming paradigm - in its pure form - offers the advantage of referential transparency. This facilitates reasoning over programs considerably. Haskell is one of the rare purely functional programming languages that is also of practical relevance. Yet, a comparable success for the verification of Haskell programs has not been achieved, so far. Unfortunately, Haskell lacks a decent theorem prover. On the other hand, the theorem prover Isabelle allows specifying functional programs in its logic HOL. We present an implementation - written in Haskell - which enables to translate Haskell programs into Isabelle/HOL theories. This approach is pragmatic, since its focus is to produce theories that are easily readable and minimise the effort to construct proofs. To this end we had to sacrifice soundness and completeness of the translation. Nevertheless, in practice this kind of translation has proven to be adequate and powerful. We also show some of the techniques that we have used for the implementation including meta programming and generic programming.

Category: Formal Verification