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 the 11th Int. Conf. on Rewriting Techniques and Applications, pp.47-61, 2000.
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 8th Int. Workshop on Termination (WST2006), pp.22-26, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00084821

F. Blanqui, Computability Closure: Ten Years Later, In Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, Rewriting, Computation and Proof), pp.68-88, 2007.

N. Dershowitz, Orderings for Term-Rewriting Systems, Theoretical Computer Science, vol.17, issue.3, pp.270-301, 1982.

J. Girard, Interprétation fonctionnelle etéliminationetélimination des coupures de l'arithmétique d'ordre supérieur, 1972.

N. Hirokawa and A. Middeldorp, Dependency Pairs Revisited, Proc. of the 15th Int. Conf. on Rewriting Techniques and Applications, pp.249-268, 2004.
DOI : 10.1007/978-3-540-25979-4_18
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.9786

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, pp.350-361, 1991.
DOI : 10.1109/LICS.1991.151659

J. Jouannaud and M. Okada, Abstract data type systems, Theoretical Computer Science, vol.173, issue.2, pp.349-391, 1997.
DOI : 10.1016/S0304-3975(96)00161-2
URL : http://doi.org/10.1016/s0304-3975(96)00161-2

K. Kusakari, M. Nakamura, and Y. Toyama, Argument Filtering Transformation, Proc. of Int. Conf. on Principles and Practice of Declarative ProgrammingPPDP'99), pp.47-61, 1999.
DOI : 10.1007/10704567_3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.8493

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 and M. Sakai, Enhancing Dependency Pair Method using Strong Computability in Simply-Typed Term Rewriting Systems, Applicable Algebra in Engineering, Communication and Computing, vol.18, issue.5, 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.235-247, 2009.
DOI : 10.1587/transinf.E92.D.235

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

A. Middeldorp, Approximations for Strategies and Termination, Proc. of the 2nd Int. Workshop on Reduction Strategies in Rewriting and Programming, 2002.
DOI : 10.1016/S1571-0661(04)80598-X
URL : http://doi.org/10.1016/s1571-0661(04)80598-x

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

M. Sakai, Y. Watanabe, and T. Sakabe, An Extension of the Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems, IEICE Transactions on Information and Systems, issue.8, pp.1025-1032, 2001.

M. Sakai and K. Kusakari, On Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems, IEICE Transactions on Information and Systems, vol.88, issue.3, pp.583-593, 2005.
DOI : 10.1093/ietisy/e88-d.3.583

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.978-989, 2007.

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

R. Thiemann, J. Giesl, and P. Schneider-kamp, Improved Modular Termination Proofs Using Dependency Pairs, Proc. of the 2nd Int. Joint Conf. on Automated Reasoning, pp.75-90, 2004.
DOI : 10.1007/978-3-540-25984-8_4
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.66.8621

X. Urbain, Modular and Incremental Automated Termination Proofs, Journal of Automated Reasoning, vol.25, issue.4, pp.315-355, 2004.
DOI : 10.1007/BF03177743