Email Gateway (Aug 18 2022 at 17:38): Email Gateway (Aug 18 2022 at 17:38):From: Will Sonnex <will@sonnex.name>
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
Last updated: Apr 30 2024 at 01:06 UTC