BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Computer Laboratory Programming Research Group Sem
 inar
SUMMARY:Termination analysis and call graph construction f
 or higher-order functional programs - Damien Seren
 i (University of Oxford)
DTSTART;TZID=Europe/London:20070622T151500
DTEND;TZID=Europe/London:20070622T161500
UID:TALK7624AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/7624
DESCRIPTION:Termination analysis for functional programs is a 
 challenging problem with applications in program v
 erification\, as well as theorem proving in which 
 it is essential to prove termination of functions 
 for soundness. Building on the size-change termina
 tion framework proposed by Lee\, Jones and Ben-Amr
 am\, we introduce termination analysis for higher-
 order functional programs\, based on a simple but 
 effective termination criterion.\n\nThe analysis a
 nd verification of higher-order programs raises th
 e issue of control-flow analysis for higher-order 
 languages. The problem of constructing an accurate
  call graph for a higher-order program has been th
 e topic of extensive research\, and the precision 
 of the call graph crucially determines the precisi
 on of the resulting analysis. Our termination fram
 ework allows the call graph construction technique
  to be varied\, and we present three constructions
  varying in precision and complexity.\n\nThere is 
 to date little theoretical understanding of the pr
 ecision of control-flow analyses. We use the expre
 ssiveness of termination analysis for each call gr
 aph to compare our control-flow analysis\, and sho
 w that precise relationships between the classes o
 f programs  recognised as terminating by the same 
 termination criterion over different call graph an
 alyses. This provides a stepping stone to a better
  understanding\nof flow analyses for higher-order 
 programs.\n
LOCATION:GS15\, Computer Laboratory
CONTACT:Viktor Vafeiadis
END:VEVENT
END:VCALENDAR