[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