Extending the loop language with higher-order procedural variables

We extend Meyer and Ritchie’s Loop language with higher-order procedures and procedural variables and we show that the resulting programming language (called Loopω) is a natural imperative counterpart of Gödel System T. The argument is two-fold: 1. we define a translation of the Loopω language into System T and we prove that this translation actually provides a lock-step simulation, 2. using a converse translation, we show that Loopω is expressive enough to encode any term of System T. Moreover, we define the “iteration rank ” of a Loopω program, which corresponds to the classical notion of “recursion rank ” in System T, and we show that both trans-lations preserve ranks. Two applications of these results in the area of implicit complexity are described.