B. Accattoli and C. Coen, On the Usefulness of Constructors, 2015.

B. Accattoli and U. Dal-lago, Beta reduction is invariant, indeed, Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, p.8, 2014.
DOI : 10.1145/2603088.2603105
URL : https://hal.archives-ouvertes.fr/hal-01091551

E. Albert, S. Genaim, and A. N. Masud, On the Inference of Resource Usage Upper and Lower Bounds, ACM Transactions on Computational Logic, vol.14, issue.3, pp.22-23
DOI : 10.1145/2499937.2499943

T. Arts and J. Giesl, Termination of term rewriting using dependency pairs, Theoretical Computer Science, vol.236, issue.1-2, pp.133-178, 2000.
DOI : 10.1016/S0304-3975(99)00207-8

D. Aspinall, L. Beringer, M. Hofmann, H. Loidl, and A. Momigliano, A program logic for resources, Theoretical Computer Science, vol.389, issue.3, pp.411-445, 2007.
DOI : 10.1016/j.tcs.2007.09.003

M. Avanzini and G. Moser, Closing the Gap Between Runtime Complexity and Polytime Computability, Proc. of 21 st RTA, pp.33-48, 2010.

M. Avanzini and G. Moser, Polynomial Path Orders, Logical Methods in Computer Science, vol.9, issue.4, p.2013
DOI : 10.2168/LMCS-9(4:9)2013
URL : http://dx.doi.org/10.2168/lmcs-9(4:9)2013

M. Avanzini and G. Moser, Tyrolean Complexity Tool: Features and Usage, Proc. of 24 th RTA, pp.71-80, 2013.

M. Avanzini and G. Moser, A Combination Framework for, Complexity. IC, 2015.

M. Avanzini, U. Dal-lago, and G. Moser, Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order (Long Version) Available at http, 2015.

F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

P. Baillot and U. Dal-lago, Higher-order interpretations and program complexity, Proc. of 26 th CSL, 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, IC, vol.207, issue.1, pp.41-62, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00012752

R. Benzinger, Automated higher-order complexity analysis, Theoretical Computer Science, vol.318, issue.1-2, pp.79-103, 2004.
DOI : 10.1016/j.tcs.2003.10.022
URL : http://doi.org/10.1016/j.tcs.2003.10.022

R. Bird, Introduction to Functional Programming using Haskell, Second Edition, 1998.

G. Bonfante, A. Cichon, J. Marion, and H. Touzet, 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 R. Péchoux, Quasi-interpretation Synthesis by Decomposition and an Application to Higher-order Programs, Proc. of 4 th ICTAC, pp.410-424, 2007.

U. , D. Lago, and M. Gaboardi, Linear Dependent Types and Relative Completeness, LMCS, vol.8, issue.4, p.2012
URL : https://hal.archives-ouvertes.fr/hal-00906347

U. , D. Lago, and S. Martini, On Constructor Rewrite Systems and the Lambda Calculus, LMCS, vol.8, issue.3, pp.1-27, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00909372

U. , D. Lago, and B. Petit, The Geometry of Types, Proc. of 40 th POPL, pp.167-178, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00909318

N. Danielsson, Lightweight semiformal time complexity analysis for purely functional data structures, Proc. of 35 th POPL, pp.133-144, 2008.

O. Danvy and L. R. Nielsen, Defunctionalization at Work, Proc. of 3 rd PPDP, pp.162-174, 2001.

J. Giesl, R. Thiemann, and P. Schneider-kamp, Proving and Disproving Termination of Higher-Order Functions, Proc. of 5 th FROCOS, pp.216-231, 2005.
DOI : 10.1007/11559306_12

J. Giesl, M. Raffelsieper, P. Schneider-kamp, S. Swiderski, and R. Thiemann, Automated termination proofs for haskell by term rewriting, ACM Transactions on Programming Languages and Systems, vol.33, issue.2, 2011.
DOI : 10.1145/1890028.1890030

G. Gomez and Y. Liu, Automatic time-bound analysis for a higher-order language, Proc. of 9 th PEPM, pp.75-86, 2002.

B. Gramlich, Abstract relations between restricted termination and confluence properties of rewrite systems, FI, vol.24, pp.3-23, 1995.

R. Harper, Practical Foundations for Programming Languages, 2012.

N. Hirokawa and G. Moser, Automated Complexity Analysis Based on the Dependency Pair Method, Proc. of 4 th IJCAR, pp.364-380, 2008.
DOI : 10.1007/978-3-540-71070-7_32

N. Hirokawa and G. Moser, Complexity, Graphs, and the Dependency Pair Method, Proc. of 15 th LPAR, pp.652-666, 2008.
DOI : 10.1007/978-3-540-89439-1_45

N. Hirokawa, A. Middeldorp, and H. Zankl, Uncurrying for Termination and Complexity, Journal of Automated Reasoning, vol.50, issue.5, pp.279-315, 2013.
DOI : 10.1007/s10817-012-9248-3

N. D. Jones, Flow analysis of lazy higher-order functional programs, Theoretical Computer Science, vol.375, issue.1-3, pp.120-136, 2007.
DOI : 10.1016/j.tcs.2006.12.030

N. D. Jones and N. Bohr, Call-by-Value Termination in the Untyped lambda-Calculus, LMCS, vol.4, issue.1, 2008.

S. Jost, K. Hammond, H. Loidl, and M. Hofmann, Static Determination of Quantitative Resource Usage for Higher-order Programs, Proc. of 37 th POPL, pp.223-236, 2010.

J. Kochems and L. Ong, Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars, Proc. of 22 nd RTA, pp.187-202, 2011.

M. Korp, C. Sternagel, H. Zankl, and A. Middeldorp, Tyrolean Termination Tool 2, Proc. of 20 th RTA, pp.295-304, 2009.
DOI : 10.1007/978-3-540-70590-1_23

J. 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

J. Midtgaard, Control-flow Analysis of Functional Programs, ACM Comput. Surv, vol.44, issue.3, p.10, 2012.

F. Nielson, H. Nielson, and C. Hankin, Principles of Program Analysis, 2005.
DOI : 10.1007/978-3-662-03811-6

L. Noschinski, F. Emmes, and J. Giesl, A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems, Proc. of 23rd CADE, LNAI, pp.422-438, 2011.
DOI : 10.1007/978-3-642-16242-8_39

C. Okasaki, Functional Pearl: Even Higher-Order Functions for Parsing, JFP, vol.8, issue.2, pp.195-199, 1998.

S. E. Panitz and M. Schmidt-schauß, TEA: Automatically proving termination of programs in a non-strict higher-order functional language, Proc. of 4 th SAS, pp.345-360, 1997.
DOI : 10.1007/BFb0032752

B. C. Pierce, Types and programming languages, 2002.

G. D. Plotkin, LCF considered as a programming language, Theoretical Computer Science, vol.5, issue.3, pp.223-255, 1977.
DOI : 10.1016/0304-3975(77)90044-5

F. Rabhi and G. Lapalme, Algorithms: A Functional Programming Approach, 1999.

J. C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference on , ACM '72, pp.363-397, 1998.
DOI : 10.1145/800194.805852

D. Sands, Complexity Analysis for a Lazy Higher-Order Language, Proc. of 3 rd ESOP, pp.361-376, 1990.

M. Sinn, F. Zuleger, and H. Veith, A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis, Proc. of 26 th CAV, pp.745-761, 2014.
DOI : 10.1007/978-3-319-08867-9_50

C. Sternagel and R. Thiemann, Generalized and Formalized Uncurrying, Proc. of 8 th FROCOS, pp.243-258, 2011.
DOI : 10.1007/978-3-642-03359-9_31

P. B. Vasconcelos and K. Hammond, Inferring Cost Equations for Recursive, Polymorphic and Higher-Order Functional Programs, Revised Papers of 15 th Workshop on IFL, pp.86-101, 2003.
DOI : 10.1007/978-3-540-27861-0_6

R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing et al., The worst-case execution-time problem???overview of methods and survey of tools, ACM Transactions on Embedded Computing Systems, vol.7, issue.3, 2008.
DOI : 10.1145/1347375.1347389

H. Zankl and M. Korp, Modular Complexity Analysis for Term Rewriting, Logical Methods in Computer Science, vol.10, issue.1, pp.1-33, 2014.
DOI : 10.2168/LMCS-10(1:19)2014