Aart Middeldorp
Proceedings of the 12th International Conference on Rewriting Techniques and Applications
RTA, 2001.

@proceedings{RTA-2001,
	address       = "Utrecht, The Netherlands",
	editor        = "Aart Middeldorp",
	isbn          = "3-540-42117-3",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 12th International Conference on Rewriting Techniques and Applications}",
	volume        = 2051,
	year          = 2001,
}

Contents (27 items)

3 ×#confluence
3 ×#higher-order
3 ×#proving
3 ×#term rewriting
3 ×#termination
2 ×#equation
2 ×#first-order
2 ×#interactive
2 ×#normalisation
2 ×#on the

RTA-2001-Barendregt #proving

Computing and Proving (HB), p. 1.

RTA-2001-Rusinowitch #deduction #verification

Rewriting for Deduction and Verification (MR), p. 2.

RTA-2001-Bechet #interactive

Universal Interaction Systems with Only Two Agents (DB), pp. 3–14.

RTA-2001-BerarducciB #algebra #higher-order #recursion

General Recursion on Second Order Term Algebras (AB, CB), pp. 15–30.

RTA-2001-BodirskyEKN #constraints #reduction

β Reduction Constraints (MB, KE, AK, JN), pp. 31–46.

RTA-2001-BonelliKR #first-order #higher-order

From Higher-Order to First-Order Rewriting (EB, DK, AR), pp. 47–62.

RTA-2001-BoudetC #algorithm

Combining Pattern E-Unification Algorithms (AB, EC), pp. 63–76.

RTA-2001-CirsteaKL

Matching Power (HC, CK, LL), pp. 77–92.

RTA-2001-GieslK #dependence #equation

Dependency Pairs for Equational Rewriting (JG, DK), pp. 93–108.

RTA-2001-Hofbauer #proving #termination

Termination Proofs by Context-Dependent Interpretations (DH), pp. 108–121.

RTA-2001-KhasidashviliOO #normalisation #orthogonal

Uniform Normalisation beyond Orthogonality (ZK, MO, VvO), pp. 122–136.

RTA-2001-KorovinV #order #using #verification

Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order (KK, AV), pp. 137–153.

RTA-2001-KuhnemannGK #cumulative #functional #source code

Relating Accumulative and Non-accumulative Functional Programs (AK, RG, KK), pp. 154–168.

RTA-2001-LevyV #equation #traversal #unification

Context Unification and Traversal Equations (JL, MV), pp. 169–184.

RTA-2001-LimetRS

Weakly Regular Relations and Applications (SL, PR, HS), pp. 185–200.

RTA-2001-Lohrey #automaton #complexity #on the #parallel

On the Parallel Complexity of Tree Automata (ML), pp. 201–215.

RTA-2001-Lucas #semantics #term rewriting

Transfinite Rewriting Semantics for Term Rewriting Systems (SL), pp. 216–230.

RTA-2001-LynchM

Goal-Directed E-Unification (CL, BM), pp. 231–245.

RTA-2001-OyamaguchiO #confluence #problem #term rewriting #unification

The Unification Problem for Confluent Right-Ground Term Rewriting Systems (MO, YO), pp. 246–260.

RTA-2001-Raamsdonk #higher-order #on the #termination

On Termination of Higher-Order Rewriting (FvR), pp. 261–275.

RTA-2001-Ringeissen #question

Matching with Free Function Symbols — A Simple Extension of Matching? (CR), pp. 276–290.

RTA-2001-Struth #calculus #transitive

Deriving Focused Calculi for Transitive Relations (GS), pp. 291–305.

RTA-2001-VestergaardB #confluence #first-order #proving #using #λ-calculus

A Formalised First-Order Confluence Proof for the λ-Calculus Using One-Sorted Variable Names (RV, JB), pp. 306–321.

RTA-2001-Woinowski #normalisation

A Normal Form for Church-Rosser Language Systems (JRW), pp. 322–337.

RTA-2001-Yamada #confluence #term rewriting #termination

Confluence and Termination of Simply Typed Term Rewriting Systems (TY), pp. 338–352.

RTA-2001-Pinto #evaluation #interactive #parallel

Parallel Evaluation of Interaction Nets with MPINE (JSP), pp. 353–356.

RTA-2001-Visser #named #program transformation #stratego

Stratego: A Language for Program Transformation Based on Rewriting Strategies (EV), pp. 357–362.