BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Zeno: An automated theorem prover for functional programs - Will S
 onnex (University of Cambridge)
DTSTART:20111011T120000Z
DTEND:20111011T130000Z
UID:TALK33701@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION:Zeno is a new tool for verifying simple properties of Haskell 
 programs through induction and other techniques\, which outputs completed 
 proofs to Isabelle. In a comparison with the rippling based tool IsaPlanne
 r and the industrial strength tool ACL2s\, using a test suite from the Isa
 Planner website\, we found that Zeno could prove\, in a timely manner\, st
 rictly more properties than either.\nIn this talk I will run through an ex
 ample proof in Zeno and discuss the heuristics we apply to select proof st
 eps and control the search space\, along with an interactive demo. You can
  try our tool out online at http://tryzeno.org
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR