J. Avenhaus and C. Loríaloría-sáenz, Higher order conditional rewriting and narrowing, Proceedings of the 1st International Conference on Constraints in Computational Logics, pp.269-284, 1994.
DOI : 10.1007/BFb0016859

F. Barbanera, M. Fernández, and H. Geuvers, Modularity of strong normalization in the algebraic-??-cube, Journal of Functional Programming, vol.7, issue.6, pp.613-660, 1997.
DOI : 10.1017/S095679689700289X

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

G. Barthe, H. Cirstea, C. Kirchner, and L. Liquori, Pure Patterns Type Systems, Principles of Programming Languages, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099463

F. Blanqui, Definitions by rewriting in the Calculus of Constructions, Mathematical Structures in Computer Science, vol.15, issue.1, pp.37-92, 2005.
DOI : 10.1017/S0960129504004426
URL : https://hal.archives-ouvertes.fr/inria-00105568

F. Blanqui, C. Kirchner, and C. Riba, On the confluence of lambda-calculus with conditional rewriting, Theoretical Computer Science, vol.411, issue.37, 2005.
DOI : 10.1016/j.tcs.2009.07.058
URL : https://hal.archives-ouvertes.fr/inria-00000729

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

V. Breazu-tannen and J. Gallier, Polymorphic Rewriting Conserves Algebraic Confluence, Information and Computation, vol.114, issue.1, pp.1-29, 1994.
DOI : 10.1006/inco.1994.1078

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

N. Dershowitz and J. Jouannaud, Rewrite Systems, Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp.243-320, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

N. Dershowitz and M. Okada, A rationale for conditional equational programming, Theoretical Computer Science, vol.75, issue.1-2, pp.111-138, 1990.
DOI : 10.1016/0304-3975(90)90064-O

D. J. Dougherty, Adding algebraic rewriting to the untyped lambda calculus, Information and Computation, vol.101, issue.2, pp.251-267, 1992.
DOI : 10.1016/0890-5401(92)90064-M

G. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/hal-01199506

B. Gramlich, On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems, Theoretical Computer Science, vol.165, issue.1, pp.97-131, 1996.
DOI : 10.1016/0304-3975(96)00042-4

J. Jouannaud and M. Okada, Executable higher-order algebraic specification languages, Proceedings of LICS'91

J. W. Klop, Combinatory Reduction Systems, Mathematical Center Tracts. CWI, vol.127, 1980.

J. W. Klop, V. Van-oostrom, and F. 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

A. Middeldorp, Completeness of Combinations of Conditional Constructor Systems, Journal of Symbolic Computation, vol.17, issue.1, pp.3-21, 1994.
DOI : 10.1006/jsco.1994.1002

F. Müller, Confluence of the lambda calculus with left-linear algebraic rewriting, Information Processing Letters, vol.41, issue.6, pp.293-299, 1992.
DOI : 10.1016/0020-0190(92)90155-O

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

E. Ohlebusch, Advanced Topics in Term Rewriting, 2002.
DOI : 10.1007/978-1-4757-3661-8

M. Takahashi, Lambda-calculi with conditional rules, TLCA'93, pp.406-417, 1993.
DOI : 10.1007/bfb0037121

V. Van-oostrom and F. Van-raamsdonk, Weak orthogonality implies confluence: The higher-order case, LFCS'94, 1994.
DOI : 10.1007/3-540-58140-5_35