Theoretical Aspects of Computer Software

Abstract

We show that simple structural conditions on proofs of convergence of equational programs, in the intrinsic-theories verificationframework of [16], correspond to resource bounds on program execution. These conditions may be construed as reflecting finitistic-predicativereasoning. The results provide a user-transparent method for certifying the computational complexity of functional programs.In particular, we define natural notions of data-positive formulas and of data-predicative derivations, and show that restrictinginduction to data-positive formulas captures precisely the primitive recursive functions, data-predicative derivations characterizethe Kalmar-elementary functions, and the combination of both yields the poly-time functions.