[Haskell-cafe] Re: ANNOUNCE zeno 0.1.0

[Luke Palmer]

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 <lrpalmer at 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 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
>>> automated inductive theorem proving tool for Haskell programs. 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.
>>>
>>> Now that it's updated it can use polymorphic types/functions, and you
>>> express properties in Haskell itself (thanks to SPJ for the
>>> suggestion). It still can't use all of Haskell's syntax: you can't
>>> have internal functions (let/where can only assign values), and you
>>> can't use type-classed polymorphic variables in function definitions -
>>> you'll have to create a monomorphic instance of the function -but I
>>> hope to have these added reasonably soon. It's also still missing
>>> primitive-types/IO/imports so it still can't be used with any
>>> real-world Haskell code, it's more a bit of theorem proving "fun".
>>>
>>> You can try it out at http://www.doc.ic.ac.uk/~ws506/tryzeno, the code
>>> file given there has some provable properties about a few prelude
>>> functions among other things.
>>>
>>> Another feature is that it lists all the sub-properties it has proven
>>> within each proof. When it verifies insertion-sort "sorted (insertsort
>>> xs) === True" it also proves the antisymmetry of "<=" and that the
>>> "insert" function preserves the "sorted" property.
>>>
>>> Any suggestions or feedback would be greatly appreciated.
>>>
>>> Cheers,
>>>
>>> Will
>>
>> -----BEGIN PGP SIGNATURE-----
>> Version: GnuPG v1.4.10 (GNU/Linux)
>>
>> iQEcBAEBAgAGBQJM3kzdAAoJEC5dcKNjBzhn6ZgH/24Yy1TBsCCtwmvItROvucms
>> VNlaJ9lAEwbFtQT4X0HJtBX0MaMc/2QcPXhXsTTXm5CG+28N7ohrVDz9WIn3Zmri
>> Tet1c+NFeZ5s4dK9Xjc450r1zlBYu6Uc8y/z9+RRbUTdDKpifGScwoxqFQPeWWYX
>> fUY9zfM6RW4W7A/hTzFIZlRpa2l8/1d4ojBeRw8PnxpPftBk8KvXAVBxq1Nf21Pc
>> pKmcfMFfhTCPAXsroLMXzP22A51XhIXrSREpvE+OgDSHsoaO+0D2/q8VMV+J1zPw
>> PPYvmM/BOYAPcjy/Z34kNv2g6letXKOjH5ofHREr5arHpsrsmJxP+rcveZWQi1A=
>> =58nx
>> -----END PGP SIGNATURE-----
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>