Skip to main content
SpringerLink
Log in

Higher-Order Rewriting

  • Conference paper
  • First Online:
Rewriting Techniques and Applications (RTA 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1631))

Included in the following conference series:

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. Aczel. A general Church-Rosser theorem. University of Manchester, July 1978.

    Google Scholar 

  2. A. Asperti and C. Laneve. Interaction systems I: The theory of optimal reductions. Mathematical Structures in Computer Science, 4:457–504, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  3. H.P. Barendregt. The Lambda Calculus, its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, revised edition, 1984.

    Google Scholar 

  4. J.A. Bergstra and J.W. Klop. Conditional rewrite rules: Confluence and termination. Journal of Computer and System Sciences, 32:323–362, 1986.

    Article  MATH  MathSciNet  Google Scholar 

  5. Alonzo Church and J.B. Rosser. Some properties of conversion. Transactions of the Americal Mathematical Society, 39:472–482, 1936.

    Article  MATH  MathSciNet  Google Scholar 

  6. N. Dershowitz. Orderings for term rewriting systems. Theoretical Computer Science, 17(3):279–301, 1982.

    Article  MATH  MathSciNet  Google Scholar 

  7. R.O. Gandy. Proofs of strong normalization. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 457–477. Academic Press, 1980.

    Google Scholar 

  8. J. Glauert and Z. Khasidashvili. Relative normalization in deterministic residual structures. In Proceedings of the 19th International Colloquium on Trees in Algebras and Programming (CAAP’ 96), volume 1059 of Lecture Notes in Computer Science, pages 180–195, April 1996.

    Google Scholar 

  9. M. Hanus and C. Prehofer. Higher-order narrowing with definitional trees. In H. Ganzinger, editor, Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA’ 96), volume 1103 of Lecture Notes in Computer Science, pages 138–152, New Brunswick, USA, 1996.

    Google Scholar 

  10. R. Hindley. Reductions of residuals are finite. Transactions of the Americal Mathematical Society, 240:345–361, June 1978.

    Article  MATH  MathSciNet  Google Scholar 

  11. G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the Association for Computing Machinery, 27(4):797–821, October 1980.

    MATH  MathSciNet  Google Scholar 

  12. G. Huet and D.C. Oppen. Equations and rewrite rules, a survey. In R.V. Book, editor, Formal Language Theory, Perspectives and Open Problems, pages 349–405. Academic Press, 1980.

    Google Scholar 

  13. J.-P. Jouannaud and A. Rubio. The higher-order recursive path ordering. In Proceedings of the 14th annual IEEE Symposium on Logic in Computer Science (LICS’ 99), Trento, Italy, 1999. To appear.

    Google Scholar 

  14. S. Kahrs. Termination proofs in an abstract setting. To appear in Mathematical Structures in Computer Science.

    Google Scholar 

  15. Z.O. Khasidashvili. Expression Reduction Systems. In Proceedings of I. Vekua Institute of Applied Mathematics, volume 36, pages 200–220, Tblisi, 1990.

    MATH  MathSciNet  Google Scholar 

  16. J.W. Klop. Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. CWI, Amsterdam, 1980. PhD Thesis.

    Google Scholar 

  17. D.E. Knuth and P.B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, 1970.

    Google Scholar 

  18. R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192:3–29, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  19. P.-A. Melliès. Description Abstraite des Systémes de Réécriture. PhD thesis, Université de Paris VII, Paris, France, 1996.

    Google Scholar 

  20. A. Middeldorp. Call by need computations to root-stable form. In Proceedings of the 24th Symposium on Principles of Programming Languages (POPL’ 97), pages 94–105, Paris, France, January 1997. ACM Press.

    Google Scholar 

  21. D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  22. T. Nipkow. Higher-order critical pairs. In Proceedings of the 6th annual IEEE Symposium on Logic in Computer Science (LICS’ 91), pages 342–349, Amsterdam, The Netherlands, July 1991.

    Google Scholar 

  23. T. Nipkow and C. Prehofer. Higher-order rewriting and equational reasoning. In W. Bibel and P. Schmitt, editors, Automated Deduction — A Basis for Applications. Volume I: Foundations, volume 8 of Applied Logic Series, pages 399–430. Kluwer, 1998.

    Google Scholar 

  24. M.J. O’Donnell. Computing in Systems Described by Equations, volume 58 of Lecture Notes in Computer Science. Springer Verlag, 1977.

    MATH  Google Scholar 

  25. V. van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhDthesis, Vrije Universiteit, Amsterdam, The Netherlands, March 1994.

    Google Scholar 

  26. V. van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159–181, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  27. V. van Oostrom. Normalisation in weakly orthogonal rewriting. In Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA’ 99), 1999.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CWI, P.O. Box 94079, 1090 GB, Amsterdam, The Netherlands

    Femke van Raamsdonk

  2. Division of Mathematics and Computer Science, Faculty of Sciences, Vrije Universiteit, De Boelelaan, 1081a, 1081, HV Amsterdam, The Netherlands

    Femke van Raamsdonk

Authors
  1. Femke van Raamsdonk
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University at Albany — SUNY, Albany, NY, 12222, USA

    Paliath Narendran

  2. LORIA — INRIA Lorraine 615, rue du Jardin Botanique, F-54602, Villers les Nancy, Cedex, France

    Michael Rusinowitch

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

van Raamsdonk, F. (1999). Higher-Order Rewriting. In: Narendran, P., Rusinowitch, M. (eds) Rewriting Techniques and Applications. RTA 1999. Lecture Notes in Computer Science, vol 1631. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48685-2_17

Download citation

  • DOI: https://doi.org/10.1007/3-540-48685-2_17

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66201-3

  • Online ISBN: 978-3-540-48685-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation