BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Termination analysis and call graph construction for higher-order 
 functional programs - Damien Sereni (University of Oxford)
DTSTART:20070622T141500Z
DTEND:20070622T151500Z
UID:TALK7624@talks.cam.ac.uk
CONTACT:Viktor Vafeiadis
DESCRIPTION:Termination analysis for functional programs is a challenging 
 problem with applications in program verification\, as well as theorem pro
 ving in which it is essential to prove termination of functions for soundn
 ess. Building on the size-change termination framework proposed by Lee\, J
 ones and Ben-Amram\, we introduce termination analysis for higher-order fu
 nctional programs\, based on a simple but effective termination criterion.
 \n\nThe analysis and verification of higher-order programs raises the issu
 e of control-flow analysis for higher-order languages. The problem of cons
 tructing an accurate call graph for a higher-order program has been the to
 pic of extensive research\, and the precision of the call graph crucially 
 determines the precision of the resulting analysis. Our termination framew
 ork allows the call graph construction technique to be varied\, and we pre
 sent three constructions varying in precision and complexity.\n\nThere is 
 to date little theoretical understanding of the precision of control-flow 
 analyses. We use the expressiveness of termination analysis for each call 
 graph to compare our control-flow analysis\, and show that precise relatio
 nships between the classes of programs  recognised as terminating by the s
 ame termination criterion over different call graph analyses. This provide
 s a stepping stone to a better understanding\nof flow analyses for higher-
 order programs.\n
LOCATION:GS15\, Computer Laboratory
END:VEVENT
END:VCALENDAR