This special issue contains selected papers presented at the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), which was held from May 30 to June 1, 2011 in Novi Sad, Serbia as part of the Federated Conference on Rewriting, Deduction, and Programming (RDP 2011). RTA is the major forum for the presentation of research on all aspects of rewriting. Six of the 20 papers presented at the conference were invited to submit an extended version to this special issue, including the paper that received the best paper award at the conference: A Rewriting View of Simple Typing by Aaron Stump, Garrin Kimmell, and Ruba El Haj Omar.

The submissions for the special issue underwent a new and thorough reviewing and revision process, in accordance with the high standards of LMCS.

• The paper Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems by Takahito Aoto and Yoshihito Toyama presents a new method for establishing confluence of rewrite systems, which is especially useful for systems incorporating associative and commutative axioms. Experiments performed with the automatic confluence prover ACP show the power of the new method.
• Patrick Bahr investigates in Modes of Convergence for Term Graph Rewriting an extension of infinitary term rewriting on term graphs. The main achievement is a generalization of two modes of convergence from terms to term graphs, showing that infinitary rewriting can smoothly be extended to term graphs.
• The paper Quantifier-Free Interpolation of a Theory of Arrays by Roberto Bruttomesso, Silvio Ghilardi and Silvio Ranise exhibits a novel method which enables easier verification of software that uses arrays. A procedure is designed that computes quantifier-free interpolants for a Skolemized version of the extensional theory of arrays, by solving equations between array updates and exploiting rewriting techniques.
• Cynthia Kop and Femke van Raamsdonk present in Dynamic Dependency Pairs for Algebraic Functional Systems a new dependency pair approach for higher-order rewriting, which includes a new technique to circumvent the subterm property that was needed in earlier work. They also extends several first-order methods, such as argument filterings and usable rules, and proposes the new method of formative rules.
• The paper Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity by Naoki Nishida, Masahiko Sakai and Toshiki Sakabe presents new sufficient conditions for the soundness of unraveling transformations from deterministic conditional rewrite systems to unconditional systems. The obtained results hold for systems with extra variables that appear naturally in the study of program inversion. To handle the additional complexity, an interesting extension of basic narrowing is considered.
• The paper A Rewriting View of Simple Typing by Aaron Stump, Garrin Kimmell, Hans Zantema and Ruba El Haj Omar is an extended, improved and corrected version of their conference paper. It sheds new light on the issues of computing types and checking typability by exploiting term rewriting methods. In particular in variants of simply-typed lambda calculi a small-step abstract reduction on terms enriched with type expressions is viewed as term rewriting and successfully analyzed.

We thank the authors and the reviewers for their hard work producing the contents of this issue, and the managing editor for special issues Benjamin Pierce for encouraging us to edit this volume.