Higher-order rewrite systems

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

2 Scopus citations


Higher-order rewrite systems are an extension of term-rewriting to (simply typed) λ-terms. This yields a formalism with a built-in notion of variable binding (λ -abstraction) and substitution (β-reduction) which is capable of describing the manipulation of terms with bound variables. Typical examples are various λ -calculi themselves, logical formulae, proof terms and programs. In this talk we survey the growing literature in this area with an emphasis on confluence results. In particular we examine some recent results by van Oostrom on very general confluence criteria which go beyond orthogonality and even generalize a result by Huet on parallel reduction between critical pairs. We also present a new critical pair condition for higher-order rewrite systems with arbitrary left-hand sides.

Original languageEnglish
Title of host publicationRewriting Techniques and Applications - 6th Intemational Conference, RTA 1995, Proceedings
EditorsJieh Hsiang
PublisherSpringer Verlag
Number of pages1
ISBN (Print)9783540592006
StatePublished - 1995
Event6th International Conference on Rewriting Techniques and Applications, RTA 1995 - Kaiserslautern, Germany
Duration: 5 Apr 19957 Apr 1995

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference6th International Conference on Rewriting Techniques and Applications, RTA 1995


Dive into the research topics of 'Higher-order rewrite systems'. Together they form a unique fingerprint.

Cite this