R. Amadio, Synthesis of max-plus quasi-interpretations, Fundam. Inform, vol.65, pp.29-60, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00146968

T. Aoto and T. Yamada, Termination of Simply Typed Term Rewriting by Translation and Labelling, RTA 2003, 2003.
DOI : 10.1007/3-540-44881-0_27

M. Avanzini, U. D. Lago, and G. Moser, Analysing the complexity of functional programs: higher-order meets first-order, ICFP 2015, pp.152-164, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01231809

M. Avanzini and G. Moser, A combination framework for complexity, RTA 2013, pp.55-70, 2013.
DOI : 10.1016/j.ic.2015.12.007

P. Baillot, M. Gaboardi, and V. Mogbil, A PolyTime Functional Language from Light Linear Logic, ESOP 2010, pp.104-124, 2010.
DOI : 10.1007/978-3-642-11957-6_7
URL : https://hal.archives-ouvertes.fr/hal-00443944

P. Baillot and U. D. Lago, Higher-order interpretations and program complexity, CSL 2012, pp.62-76, 2012.
DOI : 10.1016/j.ic.2015.12.008
URL : https://hal.archives-ouvertes.fr/hal-01337728

P. Baillot and K. Terui, Light types for polynomial time computation in lambda calculus, Information and Computation, vol.207, issue.1, pp.41-62, 2009.
DOI : 10.1016/j.ic.2008.08.005
URL : https://hal.archives-ouvertes.fr/hal-00012752

J. Stephen, S. A. Bellantoni, and . Cook, A new recursion-theoretic characterization of the poly-time functions, Computational Complexity, vol.2, pp.97-110, 1992.

J. Stephen, K. Bellantoni, H. Niggl, and . Schwichtenberg, Higher type recursion, ramification and polynomial time, Ann. Pure Appl. Logic, vol.104, issue.1-3, pp.17-30, 2000.

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

G. Bonfante, J. Marion, and J. Moyen, Quasi-interpretations a way to control resources, Theoretical Computer Science, vol.412, issue.25, pp.2776-2796, 2011.
DOI : 10.1016/j.tcs.2011.02.007
URL : https://hal.archives-ouvertes.fr/hal-00591862

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

G. Bonfante, J. Marion, and R. Péchoux, Quasiinterpretation synthesis by decomposition, ICTAC 2007, pp.410-424, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00130920

A. Brunel and K. Terui, Church => Scott = Ptime: an application of resource sensitive realizability, DICE 2010, pp.31-46, 2010.
DOI : 10.4204/EPTCS.23.3

U. Dal and L. , The geometry of linear higher-order recursion, LICS 2005, pp.366-375, 2005.

U. Dal, L. , and M. Gaboardi, Linear dependent types and relative completeness, LICS 2011, pp.133-142, 2011.

U. Dal, L. , and M. Hofmann, Realizability models and implicit complexity, Theor. Comput. Sci, vol.412, issue.20, pp.2029-2047, 2011.

U. Dal, L. , and S. Martini, Derivational complexity is an invariant cost model, FOPARA 2009, pp.88-101, 2009.

U. Dal, L. , and S. Martini, On constructor rewrite systems and the lambda-calculus, LNCS, vol.5556, pp.163-174, 2009.

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

C. Fuhs and C. Kop, Polynomial interpretations for higherorder rewriting, RTA 2012, pp.176-192, 2012.

M. Gaboardi and S. Rocca, A soft type assignment system for lambda -calculus, CSL 2007, pp.253-267, 2007.

M. Hofmann, A mixed modal/linear lambda calculus with applications to bellantoni-cook safe recursion, CSL 1997, pp.275-294, 1997.
DOI : 10.1007/BFb0028020

M. Hofmann, Safe recursion with higher types and BCK-algebra, Annals of Pure and Applied Logic, vol.104, issue.1-3, pp.113-166, 2000.
DOI : 10.1016/S0168-0072(00)00010-5

M. Hofmann, Linear types and non-size-increasing polynomial time computation, Information and Computation, vol.183, issue.1, pp.57-85, 2003.
DOI : 10.1016/S0890-5401(03)00009-9

J. and M. Okada, A computation model for executable higher-order algebraic specification languages, LICS 1991, pp.350-361, 1991.

J. Jouannaud and A. Rubio, The higher-order recursive path ordering, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.402-411, 1999.
DOI : 10.1109/LICS.1999.782635

J. W. Klop, F. Vincent-van-oostrom, and . Van-raamsdonk, Combinatory reduction systems: introduction and survey, Theoretical Computer Science, vol.121, issue.1-2, pp.279-308, 1993.
DOI : 10.1016/0304-3975(93)90091-7

D. Lankford, On proving term rewriting systems are noetherian, 1979.

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

D. Leivant and J. Marion, Lambda calculus characterizations of poly-time, Fundam. Inform, vol.19, issue.12, 1993.
DOI : 10.1007/BFb0037112

J. Marion and J. Moyen, Efficient First Order Functional Program Interpreter with Time Bound Certifications, LPAR 2000, volume 1955 of LNAI, pp.25-42, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00099178

G. Moser and A. Schnabl, The derivational complexity induced by the dependency pair method, Logical Methods in Computer Science, vol.7, issue.3, 2011.

J. Van, Termination of Higher-order Rewrite Systems, 1996.

T. Yamada, Confluence and Termination of Simply Typed Term Rewriting Systems, RTA 2001, pp.338-352, 2001.
DOI : 10.1007/3-540-45127-7_25