Vincent van Oostrom
Proceedings of the 15th International Conference on Rewriting Techniques and Applications
RTA, 2004.

@proceedings{RTA-2004,
	address       = "Aachen, Germany",
	editor        = "Vincent van Oostrom",
	isbn          = "3-540-22153-0",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 15th International Conference on Rewriting Techniques and Applications}",
	volume        = 3091,
	year          = 2004,
}

Contents (21 items)

7 ×#term rewriting
6 ×#termination
4 ×#higher-order
3 ×#named
3 ×#proving
2 ×#automation
2 ×#confluence
2 ×#unification

RTA-2004-JonesB #analysis #calculus #termination

Termination Analysis of the Untyped lamba-Calculus (NDJ, NB), pp. 1–23.

RTA-2004-Blanqui #higher-order #term rewriting #termination #type system

A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems (FB), pp. 24–39.

RTA-2004-Toyama #higher-order #lisp #term rewriting #termination

Termination of S-Expression Rewriting Systems: Lexicographic Path Ordering for Higher-Order Terms (YT), pp. 40–54.

RTA-2004-LevySV #higher-order #monad #unification

Monadic Second-Order Unification Is NP-Complete (JL, MSS, MV), pp. 55–69.

RTA-2004-Contejean #algorithm

A Certified AC Matching Algorithm (EC), pp. 70–84.

RTA-2004-Waldmann #bound #named #string

Matchbox: A Tool for Match-Bounded String Rewriting (JW), pp. 85–94.

RTA-2004-Zantema #automation #named #termination

TORPA: Termination of Rewriting Proved Automatically (HZ), pp. 95–104.

RTA-2004-CarmeNT #automaton #query

Querying Unranked Trees with Stepwise Tree Automata (JC, JN, MT), pp. 105–118.

RTA-2004-Takai #abstract interpretation #term rewriting #using #verification

A Verification Technique Using Term Rewriting Systems and Abstract Interpretation (TT), pp. 119–133.

RTA-2004-GeuversN #deduction

Rewriting for Fitch Style Natural Deductions (HG, RN), pp. 134–154.

RTA-2004-Mackie #interactive #performance

Efficient λ-Evaluation with Interaction Nets (IM), pp. 155–169.

RTA-2004-LimetS #logic programming #proving #source code #term rewriting

Proving Properties of Term Rewrite Systems via Logic Programs (SL, GS), pp. 170–184.

RTA-2004-Simonsen #composition #confluence #on the #term rewriting

On the Modularity of Confluence in Infinitary Term Rewriting (JGS), pp. 185–199.

RTA-2004-Lucas #named #proving #termination

mu-term: A Tool for Proving Termination of Context-Sensitive Rewriting (SL), pp. 200–209.

RTA-2004-GieslTSF #automation #proving #termination

Automated Termination Proofs with AProVE (JG, RT, PSK, SF), pp. 210–220.

RTA-2004-Blom #approach #approximate #λ-calculus

An Approximation Based Approach to Infinitary λ Calculi (SB), pp. 221–232.

RTA-2004-Ketema #term rewriting

Böhm-Like Trees for Term Rewriting Systems (JK), pp. 233–248.

RTA-2004-HirokawaM #dependence #revisited

Dependency Pairs Revisited (NH, AM), pp. 249–268.

RTA-2004-AotoYT #higher-order #induction #theorem

Inductive Theorems for Higher-Order Rewriting (TA, TY, YT), pp. 269–284.

RTA-2004-MitsuhashiOOY #confluence #problem #unification

The Joinability and Unification Problems for Confluent Semi-constructor TRSs (IM, MO, YO, TY), pp. 285–300.

RTA-2004-MatthewsFFF #term rewriting #visual notation

A Visual Environment for Developing Context-Sensitive Term Rewriting Systems (JM, RBF, MF, MF), pp. 301–311.