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

F. Baader and T. Nipkow, Term Rewriting and All That 9 More precisely, completion may add some epsilon transitions in this set of transitions, but the syntactical equality test can be replaced by a test modulo epsilon transition closure, 1998.

Y. Boichut, J. Chabin, and P. Réty, Over-approximating descendants by synchronized tree languages, RTA'13 Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.128-142, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00808871

Y. Boichut, R. Courbis, P. Héam, and O. Kouchnarenko, HANDLING NON LEFT-LINEAR RULES WHEN COMPLETING TREE AUTOMATA, International Journal of Foundations of Computer Science, vol.70, issue.05, 2009.
DOI : 10.1016/j.entcs.2004.07.017
URL : https://hal.archives-ouvertes.fr/hal-00561373

C. H. Broadbent, A. Carayol, M. Hague, and O. Serre, C-shore: a collapsible approach to higher-order verification, ICFP'13, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00865155

G. Castagna, K. Nguyen, Z. Xu, H. Im, S. Lenglet et al., Polymorphic functions with set-theoretic types, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, 2014.
DOI : 10.1145/2535838.2535840
URL : https://hal.archives-ouvertes.fr/hal-00907166

H. Cirstea, S. Lenglet, and P. Moreau, A faithful encoding of programmable strategies into term rewriting systems, RTA'15 Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.74-88, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01119941

H. Comon and . Sequentiality, Sequentiality, Monadic Second-Order Logic and Tree Automata, Information and Computation, vol.157, issue.1-2, pp.25-51, 2000.
DOI : 10.1006/inco.1999.2838
URL : http://doi.org/10.1006/inco.1999.2838

H. Comon and J. Rémy, How to characterize the language of ground normal forms, 1987.
URL : https://hal.archives-ouvertes.fr/inria-00075877

G. Feuillade, T. Genet, V. Viet-triem, and . Tong, Reachability Analysis over Term Rewriting Systems, Journal of Automated Reasoning, vol.37, issue.1?2, pp.3-4341, 2004.
DOI : 10.1007/s10817-004-6246-0
URL : https://hal.archives-ouvertes.fr/inria-00071609

A. Gascon, G. Godoy, and F. Jacquemard, Closure of Tree Automata Languages under Innermost Rewriting, WRS'08, pp.23-38, 2008.
DOI : 10.1016/j.entcs.2009.03.033
URL : https://hal.archives-ouvertes.fr/inria-00578966

T. Genet, Decidable approximations of sets of descendants and sets of normal forms, RTA'98, pp.151-165, 1998.
DOI : 10.1007/BFb0052368
URL : https://hal.archives-ouvertes.fr/inria-00073364

T. Genet, A note on the Precision of the Tree Automata Completion
URL : https://hal.archives-ouvertes.fr/hal-01091393

T. Genet, Towards Static Analysis of Functional Programs Using Tree Automata Completion, WRLA'14, 2014.
DOI : 10.1007/978-3-319-12904-4_8
URL : https://hal.archives-ouvertes.fr/hal-00921814

T. Genet, Termination criteria for tree automata completion, Journal of Logical and Algebraic Methods in Programming, vol.85, issue.1, pp.3-33, 2016.
DOI : 10.1016/j.jlamp.2015.05.003
URL : https://hal.archives-ouvertes.fr/hal-01194533

T. Genet, Y. Boichut, B. Boyer, V. Murat, and Y. Salmon, Reachability Analysis and Tree Automata Calculations. IRISA / Université de Rennes 1

T. Genet and R. Rusu, Equational approximations for tree automata completion, Journal of Symbolic Computation, vol.45, issue.5, pp.574-597, 2010.
DOI : 10.1016/j.jsc.2010.01.009
URL : https://hal.archives-ouvertes.fr/inria-00495405

T. Genet and Y. Salmon, Tree Automata Completion for Static Analysis of Functional Programs
URL : https://hal.archives-ouvertes.fr/hal-00780124

T. Genet and Y. Salmon, Reachability Analysis of Innermost Rewriting, RTA'15
URL : https://hal.archives-ouvertes.fr/hal-00848260

A. Geser, D. Hofbauer, J. Waldmann, and H. Zantema, On tree automata that certify termination of left-linear term rewriting systems, RTA'05, pp.353-367, 2005.

J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs et al., Proving Termination of Programs Automatically with AProVE, IJCAR'14, pp.184-191, 2014.
DOI : 10.1007/978-3-319-08587-6_13

J. Giesl, R. Thiemann, P. Schneider-kamp, and S. Falke, Mechanizing and Improving Dependency Pairs, Journal of Automated Reasoning, vol.34, issue.2, pp.155-203, 2006.
DOI : 10.1007/s10817-006-9057-7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.302

N. D. Jones and N. Andersen, 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. Kobayashi, Model Checking Higher-Order Programs, Journal of the ACM, vol.60, issue.3, p.2013
DOI : 10.1145/2487241.2487246

N. Kobayashi and A. Igarashi, Model-Checking Higher-Order Programs with Recursive Types, ESOP'13, pp.431-450, 2013.
DOI : 10.1007/978-3-642-37036-6_24

N. Kobayashi, N. Tabuchi, and H. Unno, Higher-order multi-parameter tree transducers and recursion schemes for program verification, POPL'10, pp.495-508, 2010.
DOI : 10.1145/1706299.1706355

J. Kochems and L. Ong, Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars, RTA'11 of LIPIcs. Schloss Dagstuhl?Leibniz-Zentrum fuer Informatik, 2011.

A. Lisitsa, Finite Models vs Tree Automata in Safety Verification, RTA'12, pp.225-239, 2012.

A. Middeldorp, Approximations for Strategies and Termination, Electronic Notes in Theoretical Computer Science, vol.70, issue.6, pp.1-20, 2002.
DOI : 10.1016/S1571-0661(04)80598-X
URL : http://doi.org/10.1016/s1571-0661(04)80598-x

L. Ong and S. Ramsay, Verifying higher-order functional programs with pattern-matching algebraic data types, POPL'11, 2011.
DOI : 10.1145/1925844.1926453

P. Réty, Regular Sets of Descendants for Constructor-Based Rewrite Systems, Proc. of LPAR'99, volume 1705 of LNAI, 1999.
DOI : 10.1007/3-540-48242-3_10

P. Réty and J. Vuotto, Regular Sets of Descendants by Some Rewrite Strategies, RTA'02, 2002.
DOI : 10.1007/3-540-45610-4_10

J. Reynolds, Automatic computation of data set definitions, Information Processing, vol.68, pp.456-461, 1969.

T. Takai, A Verification Technique Using Term Rewriting Systems and Abstract Interpretation, RTA'04, pp.119-133, 2004.
DOI : 10.1007/978-3-540-25979-4_9

T. Takai, Y. Kaji, and H. Seki, Right-Linear Finite Path Overlapping Term Rewriting Systems Effectively Preserve Recognizability, RTA'11, 2000.
DOI : 10.1007/10721975_17

N. Vazou, P. Rondon, and R. Jhala, Abstract Refinement Types This work is licensed under the Creative Commons Attribution-NoDerivs License. To view a copy of this license, ESOP'13 Creative Commons, 171 Second St, 2013.