Carl Christian Frederiksen, U Copenhagen, Denmark
Neil D. Jones, U Copenhagen, Denmark

Invited talk: Program analysis for implicit computational complexity

Abstract: This talk describes methods and practical work that brings
together two lines: automatic estimation of program running times, and
implicit computational complexity.  Related work has been done by
Bellantoni and Cook, Benzinger, Hofmann, Jones, Crary and Weirich, Leivant,
Marion, Niggl, Schwichtenberg, and others.  In this work we identify a
decidable class of algorithms such that all can be executed within
polynomial time (or logarithmic space).  This class includes many natural
algorithms that are used in solving real problems.  The class is properly
generalizes "safe recursion" and some related schemes provided by other
researchers.  Runtime bound information is extracted by program data-flow
analysis algorithms that extend the "size-change" framework of our POPL
2001 paper to account for running times as well as termination.  The
analysis allows automatic detection of programs that are guaranteed to run
(or be runnable) in polynomial time.