《Term Rewriting and Applications(项重写与应用/会议录)》内容简介 ：

This book constitutes the refereed proceedings of the 16th International Conference on Rewriting Techniques and Applications, RTA 2005, held in Nara, Japan in April 2005.
The 29 revised full papers and 2 systems description papers presented together with 5 invited articles were carefully reviewed and selected from 79 submissions. All current issues in Rewriting are addressed, ranging from foundational and methodological issues to applications in various contexts; due to the fact that the first RTA conference was held 20 years ago, the conference offered 3 invited historical papers 2 of which are included in this proceedings.

当当目录 ：

Confluent Term Rewriting Systems
Generalized Innermost Rewriting
Orderings for Innermost Termmation
Leanest Quasi-orderings
Abstract Modularity
Union of Equational Theories: An Algebraic Approach
Equivariant Unification
Faster Basic Syntactic Mutation with Sorts for Some Separable Equational Theories
Unification in a Class of Permutative Theories
Dependency Pairs for Simply Typed Term Rewriting
Universal Algebra for Termination of Higher-Order Rewriting
Quasi-interpretations and Small Space Bounds
A Sufficient Completeness Reasoning Tool for Partial Specifications
Tyrolean Termination Tool
Call-by-Value Is Dual to Call-by-Name - Reloaded
λu-Calculus and Duality: Call-by-Name and Call-by-Value
Reduction in a Linear Lambda-Calculus with Applications to Operational Semantics
Higher-Order Matching in the Linear Lambda Calculus in the Absence of Constants Is NP-Complete
Localized Fairness: A Rewriting Semantics
Partial Inversion of Constructor Term Rewriting Systems
Natural Narrowing for General Term Rewriting Systems
The Finite Variant Property: How to Get Rid of Some Algebraic Properties
Intruder Deduction for AC-Like Equational Theories with Homomorphisms
Proving Positive Almost-Sure Termination
Termination of Single-Threaded One-Rule Semi-Thue Systen
On Tree Automata that Certify Termination of Left-Linear Term Rewriting Systems
Twenty Years Later
Open. Closed. Open
A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code
……
Author Index