BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Automated functional program verification using fixpoint fusion - 
 Will Sonnex\, Université de Cambridge
DTSTART:20131018T141500Z
DTEND:20131018T151500Z
UID:TALK47699@talks.cam.ac.uk
CONTACT:Raphael Proust
DESCRIPTION:The current state of the art in functional program verificatio
 n uses automated proof by induction to check properties. This approach is 
 used in the well established ACL2 for Common LISP\, and the more recent Hi
 pSpec for Haskell. \n\nThis talk describes an alternative approach where t
 erms within properties are simplified until the property becomes trivially
  true. The simplification technique we use is called "fixpoint fusion"\, b
 ut also goes by the names "deforestation" and "supercompilation". We first
  present applications of this process which can verify properties at the s
 ame level as ACL2 or HipSpec. We then present an extension which allows fo
 r the fully automatic simplifications "isSorted (treesort xs) => True" and
  "isSorted (quicksort xs) => True"\, both of which it is fundamentally imp
 ossible for ACL2 or HipSpec to solve without user provided lemmas.
LOCATION:Room GC22\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR