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 <[email protected]> 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 >> [email protected] >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> >> > _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
