T. Arts and J. Giesl, Termination of term rewriting using dependency pairs, Theoretical Computer Science, vol.236, issue.1-2, pp.133-178, 2000.
DOI : 10.1016/S0304-3975(99)00207-8

F. Blanqui, Termination and Confluence of Higher-Order Rewrite Systems, Proc. of RTA'00
DOI : 10.1007/10721975_4
URL : https://hal.archives-ouvertes.fr/inria-00105556

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

F. Blanqui, Higher-order dependency pairs, Proc. of WST'06
URL : https://hal.archives-ouvertes.fr/inria-00084821

J. Giesl, R. Thiemann, P. Schneider-kamp, and S. Falke, Mechanizing and Improving Dependency Pairs, Journal of Automated Reasoning, vol.34, issue.2, pp.155-203, 2006.
DOI : 10.1007/s10817-006-9057-7

J. Giesl, P. Schneider-kamp, and R. Thiemann, AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework, Proc. IJ- CAR'06
DOI : 10.1007/11814771_24
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.2217

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

N. Hirokawa and A. Middeldorp, Tyrolean termination tool: Techniques and features, Information and Computation, pp.474-511, 2007.
DOI : 10.1016/j.ic.2006.08.010
URL : http://doi.org/10.1016/j.ic.2006.08.010

J. Jouannaud and M. Okada, A computation model for executable higher-order algebraic specification languages, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science
DOI : 10.1109/LICS.1991.151659

J. Jouannaud and A. Rubio, Higher-Order Orderings for Normal Rewriting, Proc. of RTA'06
DOI : 10.1007/11805618_29
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.537.8510

J. W. Klop, Combinatory Reduction Systems The Netherlands, 1980.

K. Kusakari, On Proving Termination of Term Rewriting Systems with Higher-Order Variables, IPSJ Transactions on Programming No. SIG, vol.42, issue.7, pp.35-45, 2001.

K. Kusakari, M. Nakamura, and Y. Toyama, Elimination Transformations for Associative- Commutative Rewriting Systems, Journal of Automated Reasoning, vol.37, issue.3, pp.205-229, 2006.

K. Kusakari and M. Sakai, Enhancing Dependency Pair Method using Strong Computability in Simply-Typed Term Rewriting Systems, Applicable Algebra in Engineering, Communication and Computing, pp.407-431, 2007.

K. Kusakari and M. Sakai, Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques, IEICE Transactions on Information and Systems, vol.92, issue.2, pp.92-235, 2009.
DOI : 10.1587/transinf.E92.D.235

K. Kusakari, Y. Isogai, M. Sakai, and F. Blanqui, Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems [17] D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification, Proceedings of the International Workshop on Extensions of Logic Programming, pp.92-2007, 1989.

R. Mayr and N. 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

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

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

T. Sakurai, K. Kusakari, M. Sakai, T. Sakabe, and N. Nishida, Usable Rules and Labeling Product-Typed Terms for Dependency Pair Method in Simply-Typed Term Rewriting Systems, IEICE Transactions on Information and Systems, issue.4, pp.90-978, 2007.