H. Comon, Completion of Rewrite Systems with Membership Constraints Part I: Deduction Rules, Journal of Symbolic Computation, vol.25, issue.4, pp.397-419, 1998.
DOI : 10.1006/jsco.1997.0185

M. William and . Farmer, A unification algorithm for second-order monadic terms, Annals of Pure and Applied Logic, vol.39, issue.2, pp.131-174, 1988.

H. Ganzinger, F. Jacquemard, and M. Veanes, Rigid Reachability, Proceedings of the 4th Asian Computing Science Conference on Advances in Computing Science, pp.4-21, 1998.
DOI : 10.1007/3-540-49366-2_2
URL : https://hal.archives-ouvertes.fr/inria-00098741

D. Warren and . Goldfarb, The undecidability of the second-order unification problem, Theor. Comput. Sci, vol.13, pp.225-230, 1981.

P. Gérard and . Huet, A unification algorithm for typed lambda-calculus, Theor. Comput. Sci, vol.1, issue.1, pp.27-57, 1975.

A. Jez, Context unification is in PSPACE, Automata, Languages, and Programming -41st International Colloquium Proceedings, Part II, pp.244-255, 2014.

J. Levy, Decidable and undecidable second-order unification problems, RTA, pp.47-60, 1998.
DOI : 10.1007/BFb0052360
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.157.7140

T. Libal, Regular patterns in second-order unification. 2015. to appear
URL : https://hal.archives-ouvertes.fr/hal-01242215

D. Miller, Unification of simply typed lambda-terms as logic programming, Eighth International Logic Programming Conference, pp.255-269, 1991.

M. Schmidt-schauß, A Decision Algorithm for Stratified Context Unification, Journal of Logic and Computation, vol.12, issue.6, pp.929-953, 2002.
DOI : 10.1093/logcom/12.6.929

M. Schmidt-schauß and K. U. Schulz, Solvability of Context Equations with Two Context Variables is Decidable, Journal of Symbolic Computation, vol.33, issue.1, pp.77-122, 2002.
DOI : 10.1006/jsco.2001.0438

M. Schmidt-schauß and K. U. Schulz, Decidability of bounded higher-order unification, Journal of Symbolic Computation, vol.40, issue.2, pp.905-954, 2005.
DOI : 10.1016/j.jsc.2005.01.005

W. Snyder and J. H. Gallier, Higher-order unification revisited: Complete sets of transformations, Journal of Symbolic Computation, vol.8, issue.1-2, pp.101-140, 1989.
DOI : 10.1016/S0747-7171(89)80023-9

M. Zaionc, The regular expression descriptions of unifier sets in the typed lambda calculus, Fundamenta Informaticae X, pp.309-322, 1987.