Higher-Order Rewriting : Framework, Confluence and Termination

In our view, the main role of higher-order rewriting is to design a type-theoretic framework in which computation and deduction are integrated by means of higher-order rewrite rules, while preserving decidability of typing and coherence of the underlying logic. The latter itself reduces to type preservation, confluence and strong normalization.

The present paper presents a unified perspective on the three existing forms of higher-order rewriting, by Klop, by Nipkow, and by Jouannaud and Okada. The comparison focuses on examples as well as on the three above properties.