R. Benzinger, Automated complexity analysis of NUPRL extracts, 1999.

D. Hofbauer and C. Lautemann, Termination proofs and the length of derivations, RTA. Number 355 in Lecture Notes in Computer Science, 1988.
DOI : 10.1007/3-540-51081-8_107

E. Cichon and P. Lescanne, Polynomial interpretations and the complexity of algorithms, CADE'11. Number 607 in Lecture Notes in Artificial Intelligence, pp.139-147, 1992.
DOI : 10.1007/3-540-55602-8_161

G. Bonfante, A. Cichon, J. Y. Marion, and H. Touzet, Algorithms with polynomial interpretation termination proof, Journal of Functional Programming, vol.11, issue.1, 2000.
DOI : 10.1017/S0956796800003877
URL : https://hal.archives-ouvertes.fr/inria-00100819

J. Y. Marion and J. Y. Moyen, Efficient first order functional program interpreter with time bound certifications, Lecture Notes in Computer Science, pp.25-42, 1955.
URL : https://hal.archives-ouvertes.fr/inria-00099178

G. Bonfante, J. Y. Marion, and J. Y. Moyen, On Lexicographic Termination Ordering with Space Bound Certifications, PSI 2001, Ershov Memorial Conference, 2001.
DOI : 10.1007/3-540-45575-2_46
URL : https://hal.archives-ouvertes.fr/inria-00100523

D. Hofbauer, Termination proofs by multiset path orderings imply primitive recursive derivation lengths, Theoretical Computer Science, vol.105, issue.1, pp.129-140, 1992.
DOI : 10.1016/0304-3975(92)90289-R

A. Weiermann, Termination proofs by lexicographic path orderings yield multiply recursive derivation lengths, Theoretical Computer Science, vol.139, pp.335-362, 1995.

A. Beckmann and A. Weiermann, A term rewriting characterization of the polytime functions and related complexity classes, Archive for Mathematical Logic, vol.36, issue.1, pp.11-30, 1996.
DOI : 10.1007/s001530050054

J. Y. Marion, Analysing the implicit complexity of programs, Information and Computation, vol.183, issue.1, pp.2-18, 2003.
DOI : 10.1016/S0890-5401(03)00011-7
URL : https://hal.archives-ouvertes.fr/inria-00099505

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

D. Leivant, Predicative recurrence and computational complexity I: Word recurrence and poly-time, Feasible Mathematics II. Birkhäuser, pp.320-343, 1994.

D. Leivant and J. Y. Marion, Lambda calculus characterizations of poly-time, Fundamenta Informaticae, vol.19, issue.167, p.184, 1993.
DOI : 10.1007/BFb0037112

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

Y. Gurevich, Algebras of feasible functions, 24th Annual Symposium on Foundations of Computer Science (sfcs 1983), pp.210-214, 1983.
DOI : 10.1109/SFCS.1983.5

R. Amadio, S. Coupet-grimal, S. D. Zilio, and L. Jakubiec, A Functional Scenario for Bytecode Verification of Resource Bounds, In: CSL, 2004.
DOI : 10.1007/978-3-540-30124-0_22
URL : https://hal.archives-ouvertes.fr/hal-00146991

R. M. Amadio and S. Dal-zilio, Resource control for synchronous cooperative threads, In: CONCUR, pp.68-82, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00146983

A. Tarski, A Decision Method for Elementary Algebra and Geometry, 1951.
DOI : 10.1007/978-3-7091-9459-1_3

R. Amadio, Max-Plus Quasi-interpretations, Lecture Notes in Computer Science, vol.2701, pp.31-45, 2003.
DOI : 10.1007/3-540-44904-3_3
URL : https://hal.archives-ouvertes.fr/hal-00146999

G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM, vol.27, issue.4, pp.797-821, 1980.
DOI : 10.1145/322217.322230

E. Grädel and Y. Gurevich, Abstract, The Journal of Symbolic Logic, vol.57, issue.03, pp.952-969, 1995.
DOI : 10.1016/0304-3975(92)90149-A

N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, issue.3, pp.279-301, 1982.
DOI : 10.1016/0304-3975(82)90026-3

M. S. Krishnamoorthy and P. Narendran, On recursive path ordering, Theoretical Computer Science, vol.40, pp.323-328, 1985.
DOI : 10.1016/0304-3975(85)90175-6
URL : http://doi.org/10.1016/0304-3975(85)90175-6

G. Bonfante, J. Y. Marion, and J. Y. Moyen, Quasi-interpretations, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00000660