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

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

H. Barendregt, Lambda calculi with types, Handbook of logic in computer science, 1992.
DOI : 10.1017/cbo9781139032636

F. Blanqui, J. Jouannaud, and M. Okada, The Calculus of Algebraic Constructions, Proc. of RTA'99
DOI : 10.1007/3-540-48685-2_25
URL : https://hal.archives-ouvertes.fr/inria-00105545

F. Blanqui, J. Jouannaud, and M. Okada, Inductive-data-type systems, Theoretical Computer Science, vol.272, issue.1-2, 1998.
DOI : 10.1016/S0304-3975(00)00347-9
URL : https://hal.archives-ouvertes.fr/inria-00105578

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

V. Breazu-tannen and J. Gallier, Polymorphic rewriting conserves algebraic strong normalization, Proc. of ICALP'89

V. Breazu-tannen and J. Gallier, Polymorphic rewriting conserves algebraic strong normalization, Theoretical Computer Science, vol.83, issue.1, 1991.

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

/. Inria-rocquencourt, /. Cnrs-/-université-paris-sud, and F. Ens-lyon, The Coq Proof Assistant Reference Manual Version 6, 1999.

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

J. Jouannaud and M. Okada, Abstract data type systems, Theoretical Computer Science, vol.173, issue.2, 1997.
DOI : 10.1016/S0304-3975(96)00161-2

J. Jouannaud and A. Rubio, The higher-order recursive path ordering, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158)
DOI : 10.1109/LICS.1999.782635

Z. Khasidashvili, Expression Reduction Systems, Proc. of I. Vekua Institute of Applied Mathematics, 1990.
URL : https://hal.archives-ouvertes.fr/hal-00148530

J. W. Klop, Combinatory Reduction Systems, 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, 1993.
DOI : 10.1016/0304-3975(93)90091-7

Z. Luo and R. Pollack, LEGO Proof Development System: User's manual, 1992.

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

N. P. Mendler, Inductive Definition in Type Theory, 1987.

D. Miller, A logic programming language with lambda-abstraction, function variables, and simple unification, Proc. of ELP'89

D. Miller and G. Nadathur, An overview of ?Prolog, Proc. of the 5th Int. Conf. on Logic Programming, 1988.

F. Müller, Confluence of the lambda calculus with left-linear algebraic rewriting, Information Processing Letters, vol.41, issue.6, p.41, 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

M. Okada, Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system, Proc. of ISSAC'89

L. Paulson, Isabelle: a generic theorem prover, LNCS, vol.828, 1994.
DOI : 10.1007/BFb0030541

W. W. Tait, Intensional interpretations of functionals of finite type I, The Journal of Symbolic Logic, vol.91, issue.02, 1967.
DOI : 10.1007/BF01447860

M. Takahashi, ??-Calculi with conditional rules, Proc. of TLCA'93
DOI : 10.1007/BFb0037121

J. Van-de-pol and H. Schwichtenberg, Strict functionals for termination proofs, Proc. of TLCA'95
DOI : 10.1007/BFb0014064

V. Van-oostrom, Confluence for Abstract and Higher-Order Rewriting, 1994.

V. Van-oostrom, Development closed critical pairs, Proc. of HOA'95, 1995.
DOI : 10.1007/3-540-61254-8_26

V. Van-oostrom and F. Van-raamsdonk, Comparing combinatory reduction systems and higher-order rewrite systems, Proc. of HOA'93
DOI : 10.1007/3-540-58233-9_13

F. Van-raamsdonk, Confluence and Normalization for Higher-Order Rewriting, 1996.

D. Wolfram, The clausal theory of types, 1990.
DOI : 10.1017/CBO9780511569906