## Jürgen Giesl

*Proceedings of the 16th International Conference on Term Rewriting and Applications*

RTA, 2005.

@proceedings{RTA-2005, address = "Nara, Japan", editor = "Jürgen Giesl", isbn = "3-540-25596-6", publisher = "{Springer International Publishing}", series = "{Lecture Notes in Computer Science}", title = "{Proceedings of the 16th International Conference on Term Rewriting and Applications}", volume = 3467, year = 2005, }

### Contents (36 items)

- RTA-2005-Toyama #confluence #term rewriting
- Confluent Term Rewriting Systems (YT), p. 1.
- RTA-2005-PolZ
- Generalized Innermost Rewriting (JvdP, HZ), pp. 2–16.
- RTA-2005-FernandezGR #order #termination
- Orderings for Innermost Termination (MLF, GG, AR), pp. 17–31.
- RTA-2005-DershowitzE #order
- Leanest Quasi-orderings (ND, ECE), pp. 32–45.
- RTA-2005-AbbottGL #composition
- Abstract Modularity (MA, NG, CL), pp. 46–60.
- RTA-2005-Hoffman #algebra #approach #equation
- Union of Equational Theories: An Algebraic Approach (PH), pp. 61–73.
- RTA-2005-Cheney #unification
- Equivariant Unification (JC), pp. 74–89.
- RTA-2005-LynchM #equation #performance
- Faster
*Basic Syntactic Mutation*with Sorts for Some Separable Equational Theories (CL, BM), pp. 90–104. - RTA-2005-TourE #unification
- Unification in a Class of Permutative Theories (TBdlT, ME), pp. 105–119.
- RTA-2005-AotoY #dependence #term rewriting
- Dependency Pairs for Simply Typed Term Rewriting (TA, TY), pp. 120–134.
- RTA-2005-Hamana #algebra #higher-order #termination
- Universal Algebra for Termination of Higher-Order Rewriting (MH), pp. 135–149.
- RTA-2005-BonfanteMM #bound
- Quasi-interpretations and Small Space Bounds (GB, JYM, JYM), pp. 150–164.
- RTA-2005-HendrixCM #reasoning #specification
- A Sufficient Completeness Reasoning Tool for Partial Specifications (JH, MC, JM), pp. 165–174.
- RTA-2005-HirokawaM #termination
- Tyrolean Termination Tool (NH, AM), pp. 175–184.
- RTA-2005-Wadler #call-by
- Call-by-Value Is Dual to Call-by-Name — Reloaded (PW), pp. 185–203.
- RTA-2005-Rocheteau #call-by #λ-calculus #μ-calculus
- λμ-Calculus and Duality: Call-by-Name and Call-by-Value (JR), pp. 204–218.
- RTA-2005-Simpson #linear #reduction #semantics #λ-calculus
- Reduction in a Linear λ-Calculus with Applications to Operational Semantics (AKS), pp. 219–234.
- RTA-2005-Yoshinaka #higher-order #linear #λ-calculus
- Higher-Order Matching in the Linear λ Calculus in the Absence of Constants Is NP-Complete (RY), pp. 235–249.
- RTA-2005-Meseguer #locality #semantics
- Localized Fairness: A Rewriting Semantics (JM), pp. 250–263.
- RTA-2005-NishidaSS #term rewriting
- Partial Inversion of Constructor Term Rewriting Systems (NN, MS, TS), pp. 264–278.
- RTA-2005-EscobarMT #term rewriting
- Natural Narrowing for General Term Rewriting Systems (SE, JM, PT), pp. 279–293.
- RTA-2005-Comon-LundhD #algebra #finite #how
- The Finite Variant Property: How to Get Rid of Some Algebraic Properties (HCL, SD), pp. 294–307.
- RTA-2005-LafourcadeLT #deduction #equation #morphism
- Intruder Deduction for
*AC*-Like Equational Theories with Homomorphisms (PL, DL, RT), pp. 308–322. - RTA-2005-BournezG #proving #termination
- Proving Positive Almost-Sure Termination (OB, FG), pp. 323–337.
- RTA-2005-MoczydlowskiG #termination #thread
- Termination of Single-Threaded One-Rule Semi-Thue Systems (WM, AG), pp. 338–352.
- RTA-2005-GeserHWZ #automaton #linear #on the #term rewriting #termination
- On Tree Automata that Certify Termination of Left-Linear Term Rewriting Systems (AG, DH, JW, HZ), pp. 353–367.
- RTA-2005-Jouannaud #years after
- Twenty Years Later (JPJ), pp. 368–375.
- RTA-2005-Dershowitz
- Open. Closed. Open (ND), pp. 376–393.
- RTA-2005-Felty #approach #semantics #tutorial
- A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code (APF), pp. 394–406.
- RTA-2005-KesnerL #paradigm
- Extending the Explicit Substitution Paradigm (DK, SL), pp. 407–422.
- RTA-2005-DowekW #modulo theories
- Arithmetic as a Theory Modulo (GD, BW), pp. 423–437.
- RTA-2005-KetemaS #combinator #reduction
- Infinitary Combinatory Reduction Systems (JK, JGS), pp. 438–452.
- RTA-2005-NieuwenhuisO #congruence
- Proof-Producing Congruence Closure (RN, AO), pp. 453–468.
- RTA-2005-StumpT #algebra #proving #similarity
- The Algebra of Equality Proofs (AS, LYT), pp. 469–483.
- RTA-2005-BouajjaniT #on the #process #reachability #set #term rewriting
- On Computing Reachability Sets of Process Rewrite Systems (AB, TT), pp. 484–499.
- RTA-2005-BonevaT #automaton #logic
- Automata and Logics for Unranked and Unordered Trees (IB, JMT), pp. 500–515.

6 ×#term rewriting

6 ×#termination

4 ×#algebra

3 ×#equation

3 ×#linear

3 ×#semantics

3 ×#λ-calculus

2 ×#approach

2 ×#automaton

2 ×#call-by

6 ×#termination

4 ×#algebra

3 ×#equation

3 ×#linear

3 ×#semantics

3 ×#λ-calculus

2 ×#approach

2 ×#automaton

2 ×#call-by