## 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)

- 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.

7 ×#term rewriting

6 ×#termination

4 ×#higher-order

3 ×#named

3 ×#proving

2 ×#automation

2 ×#confluence

2 ×#unification

6 ×#termination

4 ×#higher-order

3 ×#named

3 ×#proving

2 ×#automation

2 ×#confluence

2 ×#unification