BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Extending deforestation - William Sonnex (University of Cambridge)
DTSTART:20120306T130000Z
DTEND:20120306T140000Z
UID:TALK36225@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION:We present a technique to perform fully automated functional p
 rogram simplifications beyond what is possible through ordinary deforestat
 ion. Our implementation can so far do simplifications such as "length (ins
 ert_sort xs) => length xs" and "reverse (reverse xs) => xs". As our last p
 roperty shows\, these simplifications are for eagerly evaluated functional
  programs.\n\nWe will also show a correspondence between our extended defo
 restation\, and automated proof in dependent type theory. In effect one ca
 n use the same algorithm to both find a simplification\, and prove that th
 e simplification is sound.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR