University of Cambridge > > Computer Laboratory Programming Research Group Seminar > Termination analysis and call graph construction for higher-order functional programs

Termination analysis and call graph construction for higher-order functional programs

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Viktor Vafeiadis.

Termination analysis for functional programs is a challenging problem with applications in program verification, as well as theorem proving in which it is essential to prove termination of functions for soundness. Building on the size-change termination framework proposed by Lee, Jones and Ben-Amram, we introduce termination analysis for higher-order functional programs, based on a simple but effective termination criterion.

The analysis and verification of higher-order programs raises the issue of control-flow analysis for higher-order languages. The problem of constructing an accurate call graph for a higher-order program has been the topic of extensive research, and the precision of the call graph crucially determines the precision of the resulting analysis. Our termination framework allows the call graph construction technique to be varied, and we present three constructions varying in precision and complexity.

There 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 relationships between the classes of programs recognised as terminating by the same termination criterion over different call graph analyses. This provides a stepping stone to a better understanding of flow analyses for higher-order programs.

This talk is part of the Computer Laboratory Programming Research Group Seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2022, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity