Manfred Schmidt-Schauß
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications
RTA, 2011.

@proceedings{RTA-2011,
	address       = "Novi Sad, Serbia",
	editor        = "Manfred Schmidt-Schauß",
	ee            = "http://www.dagstuhl.de/dagpub/978-3-939897-30-9",
	isbn          = "978-3-939897-30-9",
	publisher     = "{Schloss Dagstuhl — Leibniz-Zentrum für Informatik}",
	series        = "{Leibniz International Proceedings in Informatics}",
	title         = "{Proceedings of the 22nd International Conference on Rewriting Techniques and Applications}",
	volume        = 10,
	year          = 2011,
}

Contents (31 items)

7 ×#proving
7 ×#term rewriting
4 ×#termination
3 ×#dependence
3 ×#higher-order
3 ×#named
3 ×#recursion
3 ×#source code
2 ×#analysis
2 ×#automation

RTA-2011-Tison #automaton #constraints #question #similarity #term rewriting #what

Tree Automata, (Dis-)Equality Constraints and Term Rewriting: What’s New? (ST), pp. 1–2.

RTA-2011-Tiwari

Rewriting in Practice (AT), pp. 3–8.

RTA-2011-Weirich #proving #source code

Combining Proofs and Programs (SW), p. 9.

RTA-2011-ConchinhaBC #deduction #equivalence #named #performance

FAST: An Efficient Decision Procedure for Deduction and Static Equivalence (BC, DAB, CC), pp. 11–20.

RTA-2011-ContejeanCFPU #automation #proving

Automated Certified Proofs with CiME3 (EC, PC, JF, OP, XU), pp. 21–30.

RTA-2011-DuranEEMT #maude #reachability #unification

Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6 (FD, SE, SE, JM, CLT), pp. 31–40.

RTA-2011-FalkeKS #analysis #c #compilation #source code #termination #using

Termination Analysis of C Programs Using Compiler Intermediate Languages (SF, DK, CS), pp. 41–50.

RTA-2011-GasconMR #first-order #unification

First-Order Unification on Compressed Terms (AG, SM, LR), pp. 51–60.

RTA-2011-GrathwohlKPS #graph #named #reduction #term rewriting #visualisation #λ-calculus

Anagopos: A Reduction Graph Visualizer for Term Rewriting and λ Calculus (NBBG, JK, JDP, JGS), pp. 61–70.

RTA-2011-KleinH

Maximal Completion (DK, NH), pp. 71–80.

RTA-2011-Rose #combinator #named #reduction

CRSX — Combinatory Reduction Systems with Extensions (KHR), pp. 81–90.

RTA-2011-AotoT #confluence #proving #term rewriting

A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems (TA, YT), pp. 91–106.

RTA-2011-AotoYC #higher-order #induction #theorem

Natural Inductive Theorems for Higher-Order Rewriting (TA, TY, YC), pp. 107–121.

RTA-2011-AvanziniEM #exponential #order #term rewriting

A Path Order for Rewrite Systems that Compute Exponential Time Functions (MA, NE, GM), pp. 123–138.

RTA-2011-Bahr #convergence #graph grammar

Modes of Convergence for Term Graph Rewriting (PB), pp. 139–154.

RTA-2011-BrockschmidtOG #bytecode #composition #java #proving #recursion #source code #term rewriting #termination

Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting (MB, CO, JG), pp. 155–170.

RTA-2011-BruttomessoGR #array #formal method #quantifier

Rewriting-based Quantifier-free Interpolation for a Theory of Arrays (RB, SG, SR), pp. 171–186.

RTA-2011-KochemsO #analysis #functional #linear #reachability #using

Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars (JK, CHLO), pp. 187–202.

RTA-2011-KopR #algebra #dependence #functional #higher-order

Higher Order Dependency Pairs for Algebraic Functional Systems (CK, FvR), pp. 203–218.

RTA-2011-KutsiaLV

Anti-Unification for Unranked Terms and Hedges (TK, JL, MV), pp. 219–234.

RTA-2011-MoserS #complexity #dependence #framework #multi #proving #recursion #termination

Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity (GM, AS), pp. 235–250.

RTA-2011-NeurauterM #matrix #proving #term rewriting #termination

Revisiting Matrix Interpretations for Proving Termination of Term Rewriting (FN, AM), pp. 251–266.

RTA-2011-NishidaSS #term rewriting

Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity (NN, MS, TS), pp. 267–282.

RTA-2011-NishidaV #recursion

Program Inversion for Tail Recursive Functions (NN, GV), pp. 283–298.

RTA-2011-Roux #dependence #higher-order #refinement

Refinement Types as Higher-Order Dependency Pairs (CR), pp. 299–312.

RTA-2011-SeveriV #axiom #λ-calculus

Weakening the Axiom of Overlap in Infinitary λ Calculus (PS, FJdV), pp. 313–328.

RTA-2011-SternagelT #composition #semantics

Modular and Certified Semantic Labeling and Unlabeling (CS, RT), pp. 329–344.

RTA-2011-StumpKO #confluence #problem

Type Preservation as a Confluence Problem (AS, GK, REHO), pp. 345–360.

RTA-2011-DurandS #bound #linear

Left-linear Bounded TRSs are Inverse Recognizability Preserving (ID, MS), pp. 361–376.

RTA-2011-ZanklFM #diagrams

Labelings for Decreasing Diagrams (HZ, BF, AM), pp. 377–392.

RTA-2011-ZantemaE #automation #proving #similarity

Proving Equality of Streams Automatically (HZ, JE), pp. 393–408.