Rewriting Techniques and Applications Book

	Termination analysis of the untyped [lambda]-calculus	1
	A type-based termination criterion for dependently-typed higher-order rewrite systems	24
	Termination of S-expression rewriting systems : lexicographic path ordering for higher-order terms	40
	Monadic second-order unification is NP-complete	55
	A certified AC matching algorithm	70
	Matchbox : a tool for match-bounded string rewriting	85
	TORPA : termination of rewriting proved automatically	95
	Querying unranked trees with stepwise tree automata	105
	A verification technique using term rewriting systems and abstract interpretation	119
	Rewriting for Fitch style natural deductions	134
	Efficient [lambda]-evaluation with interaction nets	155
	Proving properties of term rewrite systems via logic programs	170
	On the modularity of confluence in infinitary term rewriting	185
	MU-TERM : a tool for proving termination of context-sensitive rewriting	200
	Automated termination proofs with AProVE	210
	An approximation based approach to infinitary lambda calculi	221
	Bohm-like trees for term rewriting systems	233
	Dependency pairs revisited	249
	Inductive theorems for higher-order rewriting	269
	The joinability and unification problems for confluent semi-constructor TRSs	285
	A visual environment for developing context-sensitive term rewriting systems	301