[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,
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.
More information about the Haskell-Cafe