RTA 2011 Accepted Papers

Roberto Bruttiomesso, Silvio Ghilardi and Silvio Ranise. Rewriting-based Quantifier-free Interpolation for a Theory of Arrays
Dominik Klein and Nao Hirokawa. Maximal Completion (system description)
Stephan Falke, Deepak Kapur and Carsten Sinz. Termination Analysis of C Programs Using Compiler Intermediate Languages (system description)
Hans Zantema and Joerg Endrullis. Proving Equality of Streams Automatically
Friedrich Neurauter and Aart Middeldorp. Revisiting Matrix Interpretations for Proving Termination of Term Rewriting
Patrick Bahr. Modes of Convergence for Term Graph Rewriting
Aaron Stump, Garrin Kimmell and Roba El-Haj Omar. Type Preservation as a Confluence Problem
Adrià Gascón, Sebastian Maneth and Lander Ramos. Unif-STG: First-Order Unification on compressed terms (system description)
Naoki Nishida, Masahiko Sakai and Toshiki Sakabe. Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity
Kristoffer Rose. CRSX—Combinatory Reduction Systems with Extensions (system description)
Naoki Nishida and German Vidal. Program Inversion for Tail Recursive Functions
Paula Severi and Fer-Jan de Vries. Weakening the Axiom of Overlap in the Infinitary Lambda Calculus
Martin Avanzini, Naohi Eguchi and Georg Moser. A Path Order for Rewrite Systems that Compute Exponential Time Functions
Temur Kutsia, Jordi Levy and Mateu Villaret. Anti-Unification for Unranked Terms and Hedges
Bruno Conchinha, David Basin and Carlos Caleiro. FAST - An Efficient Decision Procedure for Deduction and Static Equivalence (system description)
Georg Moser and Andreas Schnabl. Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity
Christian Sternagel and René Thiemann. Modular and Certified Semantic Labeling and Unlabeling
Niels Bjørn Bugge Grathwohl, Jeroen Ketema, Jens Duelund Pallesen and Jakob Grue Simonsen. Anagopos: A Reduction Graph Visualizer for Term Rewriting and Lambda Calculus (system description)
Marc Sylvestre and Irène Durand. Left-linear bounded term rewriting systems are inverse recognizability preserving
Cynthia Kop and Femke Van Raamsdonk. Higher Order Dependency Pairs for Algebraic Functional Systems
Harald Zankl, Bertram Felgenhauer and Aart Middeldorp. Labelings for Decreasing Diagrams
Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons and Xavier Urbain. Automated Certified proofs with CiME3 (system description)
Marc Brockschmidt, Carsten Otto and Jürgen Giesl. Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting
Jonathan Kochems and Luke Ong. Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars
Cody Roux. Refinement Types as Higher-Order Dependency Pairs
Francisco Duran, Steven Eker, Santiago Escobar, Jose Meseguer and Carolyn Talcott. Variants, Unification, Narrowing, and Symbolic Reachability  in Maude 2.6 (system description)
Takahito Aoto, Toshiyuki Yamada and Yuki Chiba. Natural Inductive Theorems for Higher-Order Rewriting
Takahito Aoto and Yoshihito Toyama. A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems