On 11/13/10 8:15 AM, Will Sonnex wrote:
Infinite values (lazy-evaluation in general) also give Zeno a problem,
since you can no longer use structure as a well-defined ordering for
induction. A property such as reverse (reverse xs) === xs does not
work for infinite lists, since you can
Oops. It's right there on the site. My eyes skipped over it for some reason.
On Sat, Nov 13, 2010 at 2:11 PM, Luke Palmer lrpal...@gmail.com wrote:
Is the source code public, so I can run it on my own machine?
Luke
Hi all,
My masters project Zeno was recently mentioned on this mailing
However:
You can express a property such as takeWhile p xs ++ dropWhile p xs
=== xs and it will prove it to be true for all values of p :: a -
Bool and xs :: [a], over all types a, using only the function
definitions.
That is surprising, given that this property does not seem to be true
Is the source code public, so I can run it on my own machine?
Luke
Hi all,
My masters project Zeno was recently mentioned on this mailing list so
I thought I'd announce that I've just finished a major update to it,
bringing it slightly closer to being something useful. Zeno is a fully
I was wondering, Zeno capable of proving just equational statements, or is
it able to prove more general statements about programs? In particular, it
would be interesting if Zeno would be able to prove that a function is total
by verifying that it uses only structural (inductive) recursion (on
Hi Will,
I was wondering, Zeno capable of proving just equational statements, or
is it able to prove more general statements about programs? In
particular, it would be interesting if Zeno would be able to prove that
a function is total by verifying that it uses only structural
I guess I'm not on the list that received the original announce. But
I have to say, I played with the demo (
http://www.doc.ic.ac.uk/~ws506/tryzeno/ ). Wow! I am delighted and
impressed, and I think this is a huge step forward. Great work!
Luke
On Sat, Nov 13, 2010 at 1:31 AM, Petr Pudlak
Will Sonnex wrote:
Zeno is a fully automated inductive theorem proving tool for Haskell programs.
I tried it via the web interface, and it seems to be quite cool. Good work!
However:
You can express a property such as takeWhile p xs ++ dropWhile p xs
=== xs and it will prove it to be true
