[isabelle] ANNOUNCE: zeno-0.2



We've recently finished an update to Zeno, an automated theorem
proving system for Haskell program properties. It now outputs proofs
and programs as Isabelle/HOL theories and automatically invokes
Isabelle to check them. Properties to be checked are expressed in
Haskell itself, for example:

reverse_twice xs
  = prove (reverse (reverse xs) :=: xs)
elem_append xs ys y
  = givenBool (elem y ys)
  $ proveBool (elem y (xs ++ ys))

There's a much more thorough description to be found on the wiki page
(http://www.haskell.org/haskellwiki/Zeno), or you can try it online
with TryZeno (http://www.doc.ic.ac.uk/~ws506/tryzeno). I'm very
inexpert with Isabelle so I'm sure the proofs it outputs could be
improved.


Cheers,

Will





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.