When reading the paper "An applicative theory for FPH" you can encounter the following passage:
Considering theories which characterize classes of computational complexity, there are three different approaches:
- in one, the functions which can be defined within the theory are “automatically” within a certain complexity class. In such an account, the syntax has to be restricted to guarantee that one stays in the appropriate class. This results, in general, in the problem that certain definitions of functions do not work any longer, even if the function is in the complexity class under consideration.
- In a second account, the underlying logic is restricted.
- In the third account, one does not restrict the syntax, allowing, in general, to write down “function terms” for arbitrary (partial recursive) functions, nor the logic, but only for those function terms which belong to the complexity class under consideration, one can prove that they have a certain characteristic property, usually, the property that they are “provably total”. While the function terms, according to the underlying syntactical framework, may have a straightforward computational character, i.e., as $\lambda$ terms, the logic which is used to prove the characteristic property may well be classical.
My question concerns references which can be as an introduction to the three above-mentioned approaches. In this passage we see just characterizations for approaches, but do these have any generally accepted names?