[Haskell-cafe] Haskell-style proof tools?

[Sven Moritz Hallberg]

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

	http://isabelle.in.tum.de/

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:


http://scannedinavian.org/~pesco/code/transpose/Transpose.thy
This is the theory file containing the Isabelle definitions and proofs.

http://scannedinavian.org/~pesco/code/transpose/transpose.lhs
This is the original literal Haskell module. It contains the Haskell
function and a quick informal proof.


HTH,
Sven Moritz