28 Apr
2011
28 Apr
'11
8:43 p.m.
I've recently finished an update to Zeno, a proof system for Haskell program properties. It now outputs programs and proofs as Isabelle/HOL theories and should hopefully be more usable in general. You still express properties to be proven within Haskell, but the syntax has changed. Here are some examples: reverse_twice xs = prove (reverse (reverse xs) :=: xs) elem_append xs ys y = givenBool (elem y ys) $ proveBool (elem y (xs ++ ys)) Lots more details on the wiki page: http://www.haskell.org/haskellwiki/Zeno, and you can try it online using TryZeno: http://www.doc.ic.ac.uk/~ws506/tryzeno. Cheers, Will