RTA 2011 Accepted Papers
Rewriting-based Quantifier-free Interpolation for a Theory of Arrays
Maximal Completion (system description)
Termination Analysis of C Programs Using Compiler Intermediate Languages (system description)
Proving Equality of Streams Automatically
Revisiting Matrix Interpretations for Proving Termination of Term Rewriting
Modes of Convergence for Term Graph Rewriting
Type Preservation as a Confluence Problem
Unif-STG: First-Order Unification on compressed terms (system description)
Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity
CRSX—Combinatory Reduction Systems with Extensions (system description)
Program Inversion for Tail Recursive Functions
Weakening the Axiom of Overlap in the Infinitary Lambda Calculus
A Path Order for Rewrite Systems that Compute Exponential Time Functions
Anti-Unification for Unranked Terms and Hedges
FAST - An Efficient Decision Procedure for Deduction and Static Equivalence (system description)
Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity
Modular and Certified Semantic Labeling and Unlabeling
Anagopos: A Reduction Graph Visualizer for Term Rewriting and Lambda Calculus (system description)
Left-linear bounded term rewriting systems are inverse recognizability preserving
Higher Order Dependency Pairs for Algebraic Functional Systems
Labelings for Decreasing Diagrams
Automated Certified proofs with CiME3 (system description)
Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting
Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars
Refinement Types as Higher-Order Dependency Pairs
Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6 (system description)
Natural Inductive Theorems for Higher-Order Rewriting
A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems
