S. Arora and B. Barak, Computational Complexity ? A Modern Approach, 2009.

S. J. Bellantoni, K. H. Niggl, and H. Schwichtenberg, Higher type recursion, ramification and polynomial time, Annals of Pure and Applied Logic, vol.104, issue.1-3, pp.17-30, 2000.
DOI : 10.1016/S0168-0072(00)00006-3

S. Bellantoni, Predicative Recursion and The Polytime Hierarchy, Feasible Mathematics II, pp.15-29, 1995.
DOI : 10.1007/978-1-4612-2566-9_2

S. Bellantoni and S. A. Cook, A new recursion-theoretic characterization of the polytime functions, Computational Complexity, vol.106, issue.2, pp.97-110, 1992.
DOI : 10.1007/BF01201998

G. Bonfante, R. Kahle, J. Marion, and I. Oitavem, Recursion Schemata for NC k, Computer Science Logic, 22nd International Workshop, Proceedings, pp.49-63, 2008.
DOI : 10.1007/978-3-540-87531-4_6

U. Dal-lago, S. Martini, and D. Sangiorgi, Light logics and higher-order processes, 17th International Workshop on Expressiveness in Concurrency, Proceedings, 2010.
URL : https://hal.archives-ouvertes.fr/hal-01400903

U. Dal-lago, A. Masini, and M. Zorzi, Quantum implicit computational complexity, Theoretical Computer Science, vol.411, issue.2, pp.377-409, 2010.
DOI : 10.1016/j.tcs.2009.07.045

L. Fortnow and R. Santhanam, Hierarchy Theorems for Probabilistic Polynomial Time, 45th Annual IEEE Symposium on Foundations of Computer Science, pp.316-324, 2004.
DOI : 10.1109/FOCS.2004.33

J. Gill, Computational Complexity of Probabilistic Turing Machines, SIAM Journal on Computing, vol.6, issue.4, pp.675-695, 1977.
DOI : 10.1137/0206049

M. Hofmann, A mixed modal/linear lambda calculus with applications to bellantoni-cook safe recursion, Computer Science Logic, 11th International Workshop, Proceedings, volume 1414 of LNCS, pp.275-294, 1997.
DOI : 10.1007/BFb0028020

N. D. Jones, LOGSPACE and PTIME characterized by programming languages, Theoretical Computer Science, vol.228, issue.1-2, pp.151-174, 1999.
DOI : 10.1016/S0304-3975(98)00357-0

D. Leivant, Stratified functional programs and computational complexity, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '93, pp.325-333, 1993.
DOI : 10.1145/158511.158659

D. Leivant and J. Marion, Ramified recurrence and computational complexity II: Substitution and poly-space, Computer Science Logic, 9th International Workshop, Proceedings, pp.486-500, 1995.
DOI : 10.1007/BFb0022277

J. C. Mitchell, M. Mitchell, and A. Scedrov, A linguistic characterization of bounded oracle computation and probabilistic polynomial time, Proceedings 39th Annual Symposium on Foundations of Computer Science (Cat. No.98CB36280), pp.725-733, 1998.
DOI : 10.1109/SFCS.1998.743523

H. Schwichtenberg and S. Bellantoni, Feasible Computation with Higher Types, Proof and System-Reliability, pp.399-415, 2001.
DOI : 10.1007/978-94-010-0413-8_13

Y. Zhang, The computational SLR: a logic for reasoning about computational indistinguishability, Mathematical Structures in Computer Science, vol.4861, issue.05, pp.951-975, 2010.
DOI : 10.1007/BF01201998