F. Barbanera and M. Fernández, Combining first and higher order rewrite systems with type assignment systems, Proc. of the 1st Int. Conf. on Typed Lambda Calculi and Applications, 1993.
DOI : 10.1007/BFb0037098

F. Barbanera and M. Fernández, Modularity of termination and confluence in combinations of rewrite systems with ? ?, Proc. of the 20th Int. Colloq. on Automata, Languages, and Programming, 1993.

F. Barbanera, M. Fernández, and H. Geuvers, Modularity of strong normalization and confluence in the algebraic-??-cube, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, 1994.
DOI : 10.1109/LICS.1994.316049

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

F. Blanqui, Termination and Confluence of Higher-Order Rewrite Systems, Proc. of the 11th Int. Conf. on Rewriting Techniques and Applications, 2000.
DOI : 10.1007/10721975_4
URL : https://hal.archives-ouvertes.fr/inria-00105556

F. Blanqui, J. Jouannaud, and M. Okada, The Calculus of Algebraic Constructions, Proc. of the 10th Int. Conf. on Rewriting Techniques and Applications, LNCS 1631, 1999.
DOI : 10.1007/3-540-48685-2_25
URL : https://hal.archives-ouvertes.fr/inria-00105545

A. Bouhoula, J. Jouannaud, and J. Meseguer, Specification and proof in membership equational logic, Theoretical Computer Science, vol.236, 1999.
URL : https://hal.archives-ouvertes.fr/inria-00099079

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 strong normalization, Proc. of the 16th Int. Colloq. on Automata, Languages, and Programming, 1989.
DOI : 10.1016/0304-3975(91)90037-3
URL : http://doi.org/10.1016/0304-3975(91)90037-3

V. Breazu-tannen and J. Gallier, Polymorphic rewriting conserves algebraic strong normalization, Theoretical Computer Science, vol.83, issue.1, 1991.
DOI : 10.1016/0304-3975(91)90037-3
URL : http://doi.org/10.1016/0304-3975(91)90037-3

T. Coquand, Pattern matching with dependent types, Proc. of the 3rd Work. on Types for Proofs and Programs, 1992.

T. Coquand and G. Huet, Constructions: A higher order proof system for mechanizing mathematics, Proc. of the 1985 European Conf. on Computer Algebra
DOI : 10.1007/3-540-15983-5_13
URL : https://hal.archives-ouvertes.fr/inria-00076155

T. Coquand and C. Paulin-mohring, Inductively defined types, Proc. of the 1988 Int. Conf. on Computer Logic
DOI : 10.1007/3-540-52335-9_47

N. De-bruijn, The mathematical language Automath, its usage, and some of its extensions, Proc. of the Symp. on Automatic Demonstration, 1970.

N. Dershowitz and J. Jouannaud, Rewrite systems Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, 1990.

G. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo, 1998.
URL : https://hal.archives-ouvertes.fr/hal-01199506

G. Dowek and B. Werner, Proof normalization modulo, 1998.
DOI : 10.1007/3-540-48167-2_5
URL : https://hal.archives-ouvertes.fr/inria-00073143

J. Gallier, On Girard's " Candidats de Réductibilité, 1990.

E. Giménez, Codifying guarded definitions with recursion schemes, Proc. of the 5th Work. on Types for Proofs and Programs, 1994.

E. Giménez, Structural recursive definitions in type theory, Proc. of the 25th Int. Colloq. on Automata, Languages, and Programming, 1998.
DOI : 10.1007/BFb0055070

J. Girard, Une extension de l'interprétation de Gödeì a l'analyse, et son applicationàapplicationà l'´ elimination des coupures dans l'analyse et la théorie des types, Proc. of the 2nd Scandinavian Logic Symp., volume 63 of Studies in Logic and the Foundations of Mathematics, 1971.

J. Girard, Interprétation fonctionelle etéliminationetélimination des coupures dans l'arithmetique d'ordre supérieur, 1972.

J. Girard, Y. Lafont, and P. Taylor, Proofs and Types, 1988.

K. Hasebe, On extensions of Gödel's System T. Master's thesis, 2000.

J. Jouannaud and M. Okada, Executable higher-order algebraic specification languages, Proc. of the 6th Symp. on Logic in Computer Science, 1991.

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), 1999.
DOI : 10.1109/LICS.1999.782635

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

P. Martin-löf, An Intuitionistic Theory of Types: Predicative Part, Proceedings of the 73' Logic Colloquium of Studies in Logic and the Foundations of Mathematics, 1975.
DOI : 10.1016/S0049-237X(08)71945-1

P. Martin-löf, Intuitionistic type theory, Bibliopolis, 1984.

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
URL : http://doi.org/10.1016/s0304-3975(97)00143-6

N. P. Mendler, First-and second-order lambda calculi with recursive types, 1986.

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 the 1989 Int. Work. on Extensions of Logic Programming

B. Monate, Automates de formes normales et réductibilité inductive, 1997.

T. Nipkow, Higher-order critical pairs, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, 1991.
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 the 1989 Int. Symp. on Symbolic and Algebraic Computation

M. Okada and P. J. Scott, A note on rewriting theory for uniqueness of iteration, Theory and Applications of Categories, vol.6, issue.4, 2000.

C. Prehofer, Solving Higher-Order Equations: From Logic to Programming, 1995.
DOI : 10.1007/978-1-4612-1778-7

Z. Qian, Linear unification of higher-order patterns, Proc. of the 7th Int. Joint Conf. CAAP/FASE on Theory and Practice of Software Development, 1993.
DOI : 10.1007/3-540-56610-4_78

M. P. Sellink, Verifying Process Algebra Proofs in Type Theory, Proc. of the Int. Work. on Semantics of Specification Languages, Workshops in Computing, 1993.
DOI : 10.1007/978-1-4471-3229-5_18

S. Stenlund, Combinators, Lambda-Terms and Proof Theory. D. Reidel, 1972.
DOI : 10.1007/978-94-010-2913-1

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

Y. Toyama, Counterexamples to terminating for the direct sum of term rewriting systems, Information Processing Letters, vol.25, issue.3, 1986.

J. Van, Termination proofs for higher-order rewrite systems, Proc. of the 1st Int. Work. on Higher-Order Algebra, Logic and Term Rewriting, 1993.

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

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

B. Werner, Une Théorie des Constructions Inductives, 1994.