, 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
, 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
, 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
, The higher-order recursive path ordering, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158)
DOI : 10.1109/LICS.1999.782635
, 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
URL : http://doi.org/10.1016/0304-3975(93)90091-7
, 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 logic programming language with lambda-abstraction, function variables, and simple unification, Proc. of ELP'89
, On Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems, IEICE Transactions on Information and Systems, vol.88, issue.3, pp.88-583, 2005.
DOI : 10.1093/ietisy/e88-d.3.583
, An extension of dependency pair method for proving termination of higher-order rewrite systems, IEICE Transactions on Information and Systems, issue.8, pp.84-1025, 2001.
, 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
, Comparing combinatory reduction systems and higher-order rewrite systems, Proc. of HOA'93
DOI : 10.1007/3-540-58233-9_13