The Implicit Computational Complexity of Imperative Programming Languages

During the last decade Cook, Bellantoni, Leivant and others have developed the theory of implicit computational complexity, i.e. the theory of predicative recursion, tiered definition schemes, etcetera. We extend and modify this theory to work in a context of imperative programming languages, and characterise complexity classes like P, LINSPACE, PSPACE and the classes in the Grzegorczyk hiearchy. Our theoretical framework seems promising with respect to applications in engineering