Y. Boichut, B. Boyer, T. Genet, and A. Legay, Equational Abstraction Refinement for Certified Tree Regular Model Checking, ICFEM'12, 2012.
DOI : 10.1007/978-3-642-34281-3_22
URL : https://hal.archives-ouvertes.fr/hal-00759149

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

F. Chalub and C. Braga, A Modular Rewriting Semantics for CML, J.UCS, vol.10, issue.7, pp.789-807, 2004.

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/hal-01108790

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, Y. Boichut, B. Boyer, V. Murat, and Y. Salmon, Reachability Analysis and Tree Automata Calculations. IRISA / Université de Rennes 1

T. Genet, T. L. Gall, A. Legay, and V. Murat, A Completion Algorithm for Lattice Tree Automata, CIAA'13, pp.134-145, 2013.
DOI : 10.1007/978-3-642-39274-0_13

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, LIPIcs. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01194530

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

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

S. Owens, A Sound Semantics for OCamllight, ESOP'08, pp.1-15, 2008.

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