[Haskell-cafe] Haskell-style proof tools?

Sven Moritz Hallberg pesco at gmx.de
Wed Sep 21 09:44:16 EDT 2005

Robin Green schrieb:
> Does anyone know of a prover / proof assistant / proof verifier which uses a 
> vaguely Haskell-like syntax? That is to say, it allows you to express 
> theorems in Haskell-style syntax, print proof steps in Haskell-style syntax, 
> etc.

Hi Robin,

As part of a seminar, I'm currently working with Isabelle/HOL


to prove correctness of a function originally written in Haskell.
Isabelle/HOL supports a functional programming style very close to
Haskell (NB Isabelle itself is written in ML).

I'm not done yet, but I hope to make this work into a little "A
real-life example of program verification with Isabelle/HOL" paper.

As I said, it's not finished yet (by far), but I've got the termination
proof along with a couple of lemmas. I'll put the current state on the
web so you can have a look:

This is the theory file containing the Isabelle definitions and proofs.

This is the original literal Haskell module. It contains the Haskell
function and a quick informal proof.

Sven Moritz

More information about the Haskell-Cafe mailing list