Frank Pfenning
Proceedings of the 17th International Conference on Term Rewriting and Applications
RTA, 2006.

@proceedings{RTA-2006,
	address       = "Seattle, Washington, USA",
	editor        = "Frank Pfenning",
	isbn          = "3-540-36834-5",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 17th International Conference on Term Rewriting and Applications}",
	volume        = 4098,
	year          = 2006,
}

Contents (30 items)

7 ×#termination
5 ×#higher-order
4 ×#linear
3 ×#equation
3 ×#named
3 ×#proving
3 ×#term rewriting
3 ×#λ-calculus
2 ×#automation
2 ×#using

RTA-2006-Bryant #infinity #using #verification

Formal Verification of Infinite State Systems Using Boolean Methods (REB), pp. 1–3.

RTA-2006-CodishLS #constraints #partial order #termination

Solving Partial Order Constraints for LPO Termination (MC, VL, PJS), pp. 4–18.

RTA-2006-SerbanutaR

Computationally Equivalent Elimination of Conditions (TFS, GR), pp. 19–34.

RTA-2006-AntoyBC #correctness #on the

On the Correctness of Bubbling (SA, DWB, SHC), pp. 35–49.

RTA-2006-HendrixOV #automaton

Propositional Tree Automata (JH, HO, MV), pp. 50–65.

RTA-2006-GramlichL #linear #term rewriting

Generalizing Newman’s Lemma for Left-Linear Rewrite Systems (BG, SL), pp. 66–80.

RTA-2006-Hoffman #equation #monad

Unions of Equational Monadic Theories (PH), pp. 81–95.

RTA-2006-Jouannaud #composition

Modular Church-Rosser Modulo (JPJ), pp. 96–107.

RTA-2006-ChevalierR

Hierarchical Combination of Intruder Theories (YC, MR), pp. 108–122.

RTA-2006-BoichutG #approximate #re-engineering

Feasible Trace Reconstruction for Rewriting Approximations (YB, TG), pp. 123–135.

RTA-2006-BouajjaniE #modelling #source code

Rewriting Models of Boolean Programs (AB, JE), pp. 136–150.

RTA-2006-Salvati #equation #linear #type system #λ-calculus

Syntactic Descriptions: A Type System for Solving Matching Equations in the Linear λ-Calculus (SS), pp. 151–165.

RTA-2006-OhtaH #confluence #linear #λ-calculus

A Terminating and Confluent Linear λ Calculus (YO, MH), pp. 166–180.

RTA-2006-ArbiserMR #λ-calculus

A λ-Calculus with Constructors (AA, AM, AR), pp. 181–196.

RTA-2006-SantoFP #proving

Structural Proof Theory as Rewriting (JES, MJF, LP), pp. 197–211.

RTA-2006-Obua #higher-order #logic

Checking Conservativity of Overloaded Definitions in Higher-Order Logic (SO), pp. 212–226.

RTA-2006-Koprowski #higher-order #recursion

Certified Higher-Order Recursive Path Ordering (AK), pp. 227–241.

RTA-2006-Aoto #equation #induction

Dealing with Non-orientable Equations in Rewriting Induction (TA), pp. 242–256.

RTA-2006-Koprowski06a #automation #named #termination

TPA: Termination Proved Automatically (AK), pp. 257–266.

RTA-2006-ChibaA #named #program transformation #term rewriting

RAPT: A Program Transformation System Based on Term Rewriting (YC, TA), pp. 267–276.

RTA-2006-Turuani #protocol

The CL-Atse Protocol Analyser (MT), pp. 277–286.

RTA-2006-WehrmanSW #named #termination

Slothrop: Knuth-Bendix Completion with a Modern Termination Checker (IW, AS, EMW), pp. 287–296.

RTA-2006-GieslSST #analysis #automation #haskell #programming language #term rewriting #termination

Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages (JG, SS, PSK, RT), pp. 297–312.

RTA-2006-HirokawaM #predict

Predictive Labeling (NH, AM), pp. 313–327.

RTA-2006-HofbauerW #matrix #string #termination

Termination of String Rewriting with Matrix Interpretations (DH, JW), pp. 328–342.

RTA-2006-WangS #decidability #linear #termination

Decidability of Termination for Semi-constructor TRSs, Left-Linear Shallow TRSs and Related Systems (YW, MS), pp. 343–356.

RTA-2006-BournezG #proving #termination

Proving Positive Almost Sure Termination Under Strategies (OB, FG), pp. 357–371.

RTA-2006-Bruggink #finite #higher-order #product line #proving #using

A Proof of Finite Family Developments for Higher-Order Rewriting Using a Prefix Property (HJSB), pp. 372–386.

RTA-2006-JouannaudR #higher-order

Higher-Order Orderings for Normal Rewriting (JPJ, AR), pp. 387–399.

RTA-2006-LevySV #bound #higher-order #unification

Bounded Second-Order Unification Is NP-Complete (JL, MSS, MV), pp. 400–414.