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

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

7 ×#termination

5 ×#higher-order

4 ×#linear

3 ×#equation

3 ×#named

3 ×#proving

3 ×#term rewriting

3 ×#λ-calculus

2 ×#automation

2 ×#using

5 ×#higher-order

4 ×#linear

3 ×#equation

3 ×#named

3 ×#proving

3 ×#term rewriting

3 ×#λ-calculus

2 ×#automation

2 ×#using