Theories which characterize classes of computational complexity When reading the paper &quot;An applicative theory for FPH&quot; 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?
I think the first approach, the bounded arithmetic approach, is the most popular and well-studied approach. The name bounded arithmetic indicates the use of weak subsystems of Peano arithmetics, where  induction is restricted to formulas with bounded quantifiers.  I already summarized the main idea behind this approach in this post. An excellent recent reference on bounded arithmetic is the book by Cook and Nguyen, whose draft is freely available. 

The second approach uses linear logic and its subsystem as mentioned by Kaveh, which I don't know much about. 

I haven't heard of the third approach although I'm working on bounded arithmetic. But it sounds a bit strange to me since without some form of syntactic or logical restriction, how does then a theory characterize a complexity class?