An LPO-based termination ordering for higher-order terms without λ-abstraction

1. Nachum Dershowitz and Charles Hoot. Natural termination. Theoretical Computer Science, 142(2):179–207, May 1995.

   Article  MATH  MathSciNet  Google Scholar 

2. Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter 6, pages 243–320. North-Holland, Amsterdam, 1990.

   Google Scholar 

3. Stephen J. Garland and John V. Guttag. LP, the Larch Prover: Version 3.1. MIT Laboratory for Computer Science, January 1995. Available electronically at http://larch.lcs.mit.edu:8001/larch/LP/overview.html.

   Google Scholar 

4. Jean-Pierre Jouannaud and Albert Rubio. A recursive path ordering for higher-order terms in η-long Β-normal form. In Harald Ganzinger, editor, Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA-96), volume 1103 of Lecture Notes in Computer Science, pages 108–122, New Brunswick, NJ, USA, July 27–30 1996. Springer-Verlag.

   Google Scholar 

5. Jean-Pierre Jouannaud and Albert Rubio. Rewrite orderings for higher-order terms in η-long Β-normal form and the recursive path ordering. To appear in Theoretical Computer Science, 1998. Available also at http://www-lsi.upc.es/~albert/papers/horpo.ps.gz.

   Google Scholar 

6. Stefan Kahrs. Towards a domain theory for termination proofs. In Jieh Hsiang, editor, Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA-95), volume 914 of Lecture Notes in Computer Science, pages 241–255, Kaiserslautern, Germany, April 5–7 1995. Springer-Verlag.

   Google Scholar 

7. Maxim Lifantsev. Term rewriting systems. Diploma thesis, Moscow State Engineering-Physics Institute (Technical University), Moscow, Russia, February 1996. In Russian.

   Google Scholar 

8. Carlos Loria-Saenz and Joachim Steinbach. Termination of combined (rewrite and λ-calculus) systems. In MichaËl Rusinowitch and Jean-Luc Rémy, editors, Conditional Term Rewriting Systems, Third International Workshop, volume 656 of Lecture Notes in Computer Science, pages 143–147, Pont-à-Mousson, France, July 8–10, 1992. Springer-Verlag.

   Google Scholar 

9. Olav Lysne and Javier Piris. A termination ordering for higher order rewrite systems. In Jieh Hsiang, editor, Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA-95), volume 914 of Lecture Notes in Computer Science, pages 26–40, Kaiserslautern, Germany, April 5–7 1995. Springer-Verlag.

   Google Scholar 

10. M.J.C. Gordon and T.F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.

    Google Scholar 

11. Sam Owre and Natarajan Shankar. The formal semantics of PVS. Technical Report SRI-CSL-97-2, Computer Science Laboratory, SRI International, Menlo Park, CA, August 1997.

    Google Scholar 

12. Lawrence C. Paulson. Introduction to Isabelle. Technical Report 280, University of Cambridge, Computer Laboratory, 1993.

    Google Scholar 

13. Jaco Van de Pol. Termination proofs for higher-order rewrite systems. In J. Heering, K. Meinke, B. Moeller, and T. Nipkow, editors, Higher-Order Algebra, Logic, and Term Rewriting, First International Workshop, volume 816 of Lecture Notes in Computer Science, pages 350–325, Amsterdam, The Netherlands, September 1993. Springer-Verlag.

    Google Scholar 

14. Jaco Van de Pol and Helmut Schwichtenberg. Strict functionals for termination proofs. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science, pages 350–364, Edinburgh, Scotland, April 1995. Springer-Verlag.

    Google Scholar 

Download references