Compexity Classes and Higher Types

We introduce an imperative programming language equipped with variables of higher types. Fragments of this language characterize complexity classes (including the small and important classes LOGSPACE, LINSPACE, PSPACE, P, EXP). Furthermore, we show how the same complexity classes can be characterized by fragments of Gödel's system T. All our characterizations can be dubbed implicit since they are purely syntactical with no references to explicit resource bounds