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