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

J. Boichut, P. Chabin, and . 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

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

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

K. Castagna, Z. Nguyen, H. Xu, S. Im, L. 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

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

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

G. Gascon, F. Godoy, and . 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

. 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

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

. 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

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

R. Genet and . 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

Y. Genet and . Salmon, Reachability Analysis of Innermost Rewriting
URL : https://hal.archives-ouvertes.fr/hal-01194530

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

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

M. Giesl, F. Brockschmidt, F. Emmes, C. 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

R. Giesl, P. Thiemann, S. Schneider-kamp, and . 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

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

. Kobayashi, Model Checking Higher-Order Programs, Journal of the ACM, vol.60, issue.3, p.2013
DOI : 10.1145/2487241.2487246

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

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

. 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

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

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

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

P. Vazou, R. Rondon, and . Jhala, Abstract Refinement Types, ESOP'13, 2013.
DOI : 10.1007/978-3-642-37036-6_13