Higher-Order Rewriting and Equational Reasoning

Tobias Nipkow and Christian Prehofer

From the introduction:
The objective of this chapter is to survey the results which have been generalized from first-order to higher-order rewrite systems. The aim of this generalization is to lift the rich theory developed around first-order rewrite systems and apply it to systems manipulating higher-order terms, such as program transformers, theorem provers and the like. We will consider the basic properties and techniques and focus on confluence results and equational reasoning.

BibTeX:

@incollection{Nipkow-Prehofer,
author={Tobias Nipkow and Christian Prehofer},
title={Higher-Order Rewriting and Equational Reasoning},
booktitle={Automated Deduction --- A Basis for Applications.
           Volume I: Foundations},
editor={W. Bibel and P. Schmitt},
publisher={Kluwer},
series={Applied Logic Series},
volume=8,
year=1998,
pages={399--430}}