Higher-order rewrite systems

Tobias Nipkow

doi:10.1007/3-540-59200-8_61

Higher-order rewrite systems

Tobias Nipkow

Informatics 7 - Chair of Theoretical Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

3 Scopus citations

Abstract

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 language	English
Title of host publication	Rewriting Techniques and Applications - 6th Intemational Conference, RTA 1995, Proceedings
Editors	Jieh Hsiang
Publisher	Springer Verlag
Pages	256
Number of pages	1
ISBN (Print)	9783540592006
DOIs	https://doi.org/10.1007/3-540-59200-8_61
State	Published - 1995
Event	6th International Conference on Rewriting Techniques and Applications, RTA 1995 - Kaiserslautern, Germany Duration: 5 Apr 1995 → 7 Apr 1995

Publication series

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

Conference

Conference	6th International Conference on Rewriting Techniques and Applications, RTA 1995
Country/Territory	Germany
City	Kaiserslautern
Period	5/04/95 → 7/04/95

Access to Document

10.1007/3-540-59200-8_61

Cite this

Nipkow, T. (1995). Higher-order rewrite systems. In J. Hsiang (Ed.), Rewriting Techniques and Applications - 6th Intemational Conference, RTA 1995, Proceedings (pp. 256). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 914). Springer Verlag. https://doi.org/10.1007/3-540-59200-8_61

@inproceedings{87eb23cec6d3452d90e82eedbece9608,

title = "Higher-order rewrite systems",

abstract = "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.",

author = "Tobias Nipkow",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1995.; 6th International Conference on Rewriting Techniques and Applications, RTA 1995 ; Conference date: 05-04-1995 Through 07-04-1995",

year = "1995",

doi = "10.1007/3-540-59200-8_61",

language = "English",

isbn = "9783540592006",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "256",

editor = "Jieh Hsiang",

booktitle = "Rewriting Techniques and Applications - 6th Intemational Conference, RTA 1995, Proceedings",

}

Nipkow, T 1995, Higher-order rewrite systems. in J Hsiang (ed.), Rewriting Techniques and Applications - 6th Intemational Conference, RTA 1995, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 914, Springer Verlag, pp. 256, 6th International Conference on Rewriting Techniques and Applications, RTA 1995, Kaiserslautern, Germany, 5/04/95. https://doi.org/10.1007/3-540-59200-8_61

Higher-order rewrite systems. / Nipkow, Tobias.
Rewriting Techniques and Applications - 6th Intemational Conference, RTA 1995, Proceedings. ed. / Jieh Hsiang. Springer Verlag, 1995. p. 256 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 914).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Higher-order rewrite systems

AU - Nipkow, Tobias

PY - 1995

Y1 - 1995

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84955561398&partnerID=8YFLogxK

U2 - 10.1007/3-540-59200-8_61

DO - 10.1007/3-540-59200-8_61

M3 - Conference contribution

AN - SCOPUS:84955561398

SN - 9783540592006

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 256

BT - Rewriting Techniques and Applications - 6th Intemational Conference, RTA 1995, Proceedings

A2 - Hsiang, Jieh

PB - Springer Verlag

T2 - 6th International Conference on Rewriting Techniques and Applications, RTA 1995

Y2 - 5 April 1995 through 7 April 1995

ER -

Higher-order rewrite systems

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this