A. Boudet, Combining Unification Algorithms, Journal of Symbolic Computation, vol.16, issue.6, pp.597-626, 1993.
DOI : 10.1006/jsco.1993.1066

A. Boudet and E. Contejean, ???Syntactic??? AC-unification, Jouannaud [11], pp.136-151
DOI : 10.1007/BFb0016849
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.8487

A. Boudet and E. Contejean, AC-unification of higher-order patterns, Principles and Practice of Constraint Programming, pp.267-281, 1997.
DOI : 10.1007/BFb0017445

A. Boudet and E. Contejean, About the confluence of equational pattern rewrite systems, 15th International Conference on Automated Deduction, pp.88-102, 1998.
DOI : 10.1007/BFb0054250

V. Breazu-tannen, Combining algebra and higher-order types, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, 1988.
DOI : 10.1109/LICS.1988.5103

H. Comon, M. Haberstrau, and J. Jouannaud, Syntacticness, Cycle-Syntacticness, and Shallow Theories, Information and Computation, vol.111, issue.1, pp.154-191, 1994.
DOI : 10.1006/inco.1994.1043
URL : http://doi.org/10.1006/inco.1994.1043

G. Dowek, Third order matching is decidable, Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pp.2-10, 1992.

D. Warren and . Goldfarb, Note on the undecidability of the second-order unification problem, Theoretical Computer Science, vol.13, pp.225-230, 1981.

R. Hindley and J. Seldin, Introduction to Combinators and ?-calculus, 1986.
DOI : 10.1017/CBO9780511809835

G. Huet, Résolution d'´ equations dans les langages d'ordre 1? 2? ? ? ?, Thèse d'Etat, 1976.

J. and C. Kirchner, Solving equations in abstract algebras: A rule-based survey of unification, Computational Logic: Essays in Honor of Alan Robinson, 1991.

C. Kirchner, Méthodes et outils de conception systématique d'algorithmes d'unification dans les théories equationnelles, Thèse d'Etat, 1985.

C. Kirchner, Computing unification algorithms, Proc. 1st IEEE Symp. Logic in Computer Science, pp.206-216, 1986.

C. Kirchner and F. Klay, Syntactic theories and unification, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, 1990.
DOI : 10.1109/LICS.1990.113753

R. Mayr and T. Nipkow, Higher-order rewrite systems and their confluence, Theoretical Computer Science, vol.192, issue.1, pp.3-29, 1998.
DOI : 10.1016/S0304-3975(97)00143-6
URL : http://doi.org/10.1016/s0304-3975(97)00143-6

D. Miller, A logic programming language with lambda-abstraction, function variables, and simple unification, Extensions of Logic Programming, 1991.

T. Nipkow, Higher-order critical pairs, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, 1991.
DOI : 10.1109/LICS.1991.151658

V. Padovani, Filtrage d'ordre supérieur, 1996.

G. Plotkin, Building-in equational theories, Machine Intelligence, vol.7, 1972.

Z. Qian and K. Wang, Modular AC unification of higher-order patterns, Jouannaud [11], pp.105-120
DOI : 10.1007/BFb0016847

M. Schmidt-schauß, Unification in a combination of arbitrary disjoint equational theories, Journal of Symbolic Computation, 1990.

H. Jörg and . Siekmann, Unification theory, Journal of Symbolic Computation, vol.7, issue.3, 1989.

E. Tidén and S. Arnborg, Unification problems with one-sided distributivity, Journal of Symbolic Computation, vol.3, issue.1-2, pp.183-202, 1987.
DOI : 10.1016/S0747-7171(87)80026-3