P. Aczel, A general Church-Rosser theorem, 1978.

H. Barendregt, The Lambda-Calculus, its syntax and semantics. Studies in Logic and the 831 Foundation of Mathematics, 1984.

L. Baxter, The complexity of unification, Thèse de doctorat, pp.1977-2006

J. Hans-jürgen and . Bürckert, Matching ? A special case of unification? In Unification, pp.125-138, 1990.

H. Cirstea and C. Kirchner, The rewriting calculus - part II, Logic Journal of IGPL, vol.9, issue.3, pp.427-498, 1933.
DOI : 10.1093/jigpal/9.3.377
URL : https://hal.archives-ouvertes.fr/inria-00100532

R. Curien, Z. Qian, and H. Shi, Efficient second-order matching, Rewriting Tech- 839 niques and Applications -RTA'96, p.27, 1996.
DOI : 10.1007/3-540-61464-8_62

J. Despeyroux, Natural semantics: specifications and proofs, p.842

G. Dowek, T. Hardin, and C. Kirchner, Higher Order Unification via Explicit Substitutions, Information and Computation, vol.157, issue.1-2, pp.183-235, 2000.
DOI : 10.1006/inco.1999.2837
URL : https://hal.archives-ouvertes.fr/hal-01199528

O. De, M. , and G. Sittampalam, Higher-order matching for program transformation, p.846

G. Dowek, Third order matching is decidable, Annals of Pure and Applied Logic, vol.69, issue.2-3, pp.135-155, 1994.
DOI : 10.1016/0168-0072(94)90083-3
URL : http://doi.org/10.1016/0168-0072(94)90083-3

G. Dowek, Higher-Order Unification and Matching, Handbook of Automated Reasoning, p.850
DOI : 10.1016/B978-044450813-3/50018-7

M. Dalrymple, S. M. Shieber, and F. Pereira, Ellipsis and higher-order unification, Linguistics and Philosophy, vol.8, issue.1, pp.399-452, 1991.
DOI : 10.1007/BF00630923
URL : http://arxiv.org/abs/cmp-lg/9503008

G. Faure, Matching Modulo Superdevelopments Application to Second-Order Matching, 854 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning 855 -LPAR'06, pp.60-74, 2006.
DOI : 10.1007/11916277_5

G. Faure, Structure et modèles de calcul de réécriture, Thèse de doctorat

D. Goldfarb, The undecidability of the second order unification, Journal of Theoretical Computer Science, vol.859, issue.13 11, pp.225-230, 1981.

G. Huet and B. Lang, Proving and applying program transformations expressed with 861 second-order patterns, Acta Informatica, vol.11, issue.26, pp.17-27, 1978.

G. Huet, A mechanization of type theory, Proceedings of the 3rd 863

G. Huet, Résolution d'´ equations dans les langages d'ordre 1, Thèse de doctorat 866 d'´ etat, p.27, 1975.

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

C. Kirchner, A new equational unification method: A generalization of martelli-montanari's 873 algorithm, pp.224-247, 1984.

J. W. Klop, Combinatory Reduction Systems, Mathematisch Centrum, Am- 875 sterdam, 1980.

K. Klop, F. Vincent-van-oostrom, and . Van-raamsdonk, Combinatory reduction systems: introduction and survey, Theoretical Computer Science, vol.121, issue.1-2, pp.279-308, 1993.
DOI : 10.1016/0304-3975(93)90091-7
URL : http://doi.org/10.1016/0304-3975(93)90091-7

J. Lévy, Reductions Correctes et Optimales dans le Lambda-Calcul, 1978.

R. Loader, Higher Order ?? Matching is Undecidable, Logic Journal of IGPL, vol.11, issue.1, pp.51-881, 2003.
DOI : 10.1093/jigpal/11.1.51
URL : http://jigpal.oxfordjournals.org/cgi/content/short/11/1/51

D. Miller, Higher-order logic programming, Int. Conf. on Logic Programming, p.784, 1990.
DOI : 10.1007/3-540-16492-8_94
URL : https://hal.archives-ouvertes.fr/hal-00776197

D. Miller, A logic programming language with lambda-abstraction, function variables, and 885 simple unification, Journal of Logic and Computation, issue.2, p.14, 1991.

A. Martelli and U. Montanari, An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems, vol.4, issue.2, p.887
DOI : 10.1145/357162.357169

R. Mayr and T. Nipkow, Higher-order rewrite systems and their confluence, Theoretical 889 Computer Science, p.32, 1998.
DOI : 10.1016/S0304-3975(97)00143-6
URL : http://doi.org/10.1016/s0304-3975(97)00143-6

T. Nipkow and C. Prehofer, Higher-order rewriting and equational reasoning, p.891

V. Van and O. , Confluence for abstract and higher-order rewriting, p.32, 1994.

V. Padovani, Decidability of fourth-order matching, Mathematical Structures in Computer Science, vol.10, issue.3
DOI : 10.1017/S0960129500003108
URL : https://hal.archives-ouvertes.fr/hal-00527853

F. Pfenning, Logical Frameworks, Handbook of Automated Reasoning, pp.1063-1147, 2001.
DOI : 10.1016/B978-044450813-3/50019-9

Z. Qian, Unification of higher-order patterns in linear time and space, Journal of Logic and Computation, vol.6, issue.3, p.14, 1996.
DOI : 10.1093/logcom/6.3.315

W. Snyder and J. Gallier, Higher-order unification revisited: Complete sets of transfor- 901 mations, JSCOMP: Journal of Symbolic Computation, vol.8, issue.15, p.27, 1989.

H. Shi, Extended matching with applications to program transformation, 1994.

G. Sittampalam, Higher-order Matching for Program Transformation, Mag- 905 dalen College, p.3, 2001.

C. Stirling, Decidability of higher-order matching, Logical Methods in Computer Science, vol.5, issue.3, p.14, 2009.
DOI : 10.2168/LMCS-5(3:2)2009

E. Visser, A survey of strategies in rule-based program transformation systems, Journal of 911 Symbolic Computation, 2005.
DOI : 10.1016/j.jsc.2004.12.011

V. Van, O. , and F. Van-raamsdonk, Comparing combinatory reduction systems 913 and higher-order rewrite systems, Femke van Raamsdonk. Confluence and superdevelopments, pp.912-915, 1993.