17. RTA 2006: Seattle, WA, USA

FLoC Plenary Talk

• Randal E. Bryant:
  Formal Verification of Infinite State Systems Using Boolean Methods. 1-3
  

Session 1. Constraints and Optimization

• Michael Codish, Vitaly Lagoon, Peter J. Stuckey:
  Solving Partial Order Constraints for LPO Termination. 4-18
  
• Traian-Florin Serbanuta, Grigore Rosu:
  Computationally Equivalent Elimination of Conditions. 19-34
  
• Sergio Antoy, Daniel W. Brown, Su-Hui Chiang:
  On the Correctness of Bubbling. 35-49
  
• Joe Hendrix, Hitoshi Ohsaki, Mahesh Viswanathan:
  Propositional Tree Automata. 50-65
  

Session 2. Equational Reasoning

• Bernhard Gramlich, Salvador Lucas:
  Generalizing Newman's Lemma for Left-Linear Rewrite Systems. 66-80
  
• Piotr Hoffman:
  Unions of Equational Monadic Theories. 81-95
  
• Jean-Pierre Jouannaud:
  Modular Church-Rosser Modulo. 96-107
  

Session 3. System Verification

• Yannick Chevalier, Michaël Rusinowitch:
  Hierarchical Combination of Intruder Theories. 108-122
  
• Yohan Boichut, Thomas Genet:
  Feasible Trace Reconstruction for Rewriting Approximations. 123-135
  

Invited Talk

• Ahmed Bouajjani, Javier Esparza:
  Rewriting Models of Boolean Programs. 136-150
  

Session 4. Lambda Calculus

• Sylvain Salvati:
  Syntactic Descriptions: A Type System for Solving Matching Equations in the Linear lambda-Calculus. 151-165
  
• Yo Ohta, Masahito Hasegawa:
  A Terminating and Confluent Linear Lambda Calculus. 166-180
  
• Ariel Arbiser, Alexandre Miquel, Alejandro Ríos:
  A Lambda-Calculus with Constructors. 181-196
  
• José Espírito Santo, Maria João Frade, Luis Pinto:
  Structural Proof Theory as Rewriting. 197-211
  

Session 5. Theorem Proving

• Steven Obua:
  Checking Conservativity of Overloaded Definitions in Higher-Order Logic. 212-226
  
• Adam Koprowski:
  Certified Higher-Order Recursive Path Ordering. 227-241
  
• Takahito Aoto:
  Dealing with Non-orientable Equations in Rewriting Induction. 242-256
  

Session 6. System Descriptions

• Adam Koprowski:
  TPA: Termination Proved Automatically. 257-266
  
• Yuki Chiba, Takahito Aoto:
  RAPT: A Program Transformation System Based on Term Rewriting. 267-276
  
• Mathieu Turuani:
  The CL-Atse Protocol Analyser. 277-286
  
• Ian Wehrman, Aaron Stump, Edwin M. Westbrook:
  Slothrop: Knuth-Bendix Completion with a Modern Termination Checker. 287-296
  

Invited Talk

• Jürgen Giesl, Stephan Swiderski, Peter Schneider-Kamp, René Thiemann:
  Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages. 297-312
  

Session 6. System Descriptions

• Nao Hirokawa, Aart Middeldorp:
  Predictive Labeling. 313-327
  
• Dieter Hofbauer, Johannes Waldmann:
  Termination of String Rewriting with Matrix Interpretations. 328-342
  
• Yi Wang, Masahiko Sakai:
  Decidability of Termination for Semi-constructor TRSs, Left-Linear Shallow TRSs and Related Systems. 343-356
  
• Olivier Bournez, Florent Garnier:
  Proving Positive Almost Sure Termination Under Strategies. 357-371
  

Session 8. Higher-Order Rewriting and Unification

• Harrie Jan Sander Bruggink:
  A Proof of Finite Family Developments for Higher-Order Rewriting Using a Prefix Property. 372-386
  
• Jean-Pierre Jouannaud, Albert Rubio:
  Higher-Order Orderings for Normal Rewriting. 387-399
  
• Jordi Levy, Manfred Schmidt-Schauß, Mateu Villaret:
  Bounded Second-Order Unification Is NP-Complete. 400-414