[Haskell] ANNOUNCE: zeno-0.2

Will Sonnex ws506 at doc.ic.ac.uk
Thu Apr 28 22:43:14 CEST 2011


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



More information about the Haskell mailing list