%{search_type} search results

• Process Types as a Descriptive Tool for Interaction: Control and the Pi-Calculus
• Concurrent Programming Languages and Methods for Semantic Analyses (Extended Abstract of Invited Talk)
• Unnesting of Copatterns
• Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams
• Predicate Abstraction of Rewrite Theories
• Unification and Logarithmic Space
• Ramsey Theorem as an Intuitionistic Property of Well Founded Relations
• A Model of Countable Nondeterminism in Guarded Type Theory
• Cut Admissibility by Saturation
• Automatic Evaluation of Context-Free Grammars (System Description)
• Tree Automata with Height Constraints between Brothers
• A Coinductive Confluence Proof for Infinitary Lambda-Calculus
• An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting
• Preciseness of Subtyping on Intersection and Union Types
• Abstract Datatypes for Real Numbers in Type Theory
• Self Types for Dependently Typed Lambda Encodings
• First-Order Formative Rules
• Automated Complexity Analysis Based on Context-Sensitive Rewriting
• Amortised Resource Analysis and Typed Polynomial Interpretations
• Confluence by Critical Pair Analysis
• Proof Terms for Infinitary Rewriting
• Construction of Retractile Proof Structures
• Local States in String Diagrams
• Reduction System for Extensional Lambda-mu Calculus
• The Structural Theory of Pure Type Systems
• Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB
• Implicational Relevance Logic is 2-ExpTime-Complete
• Near Semi-rings and Lambda Calculus
• All-Path Reachability Logic
• Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
• Conditional Confluence (System Description)
• Nagoya Termination Tool
• Termination of Cycle Rewriting.

This book constitutes the refereed proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications, RTA 2014, and 12th International Conference on Typed Lambda-Calculi and Applications, TLCA 2014, held as part of the Vienna Summer of Logic, VSL 2014, in Vienna, Austria, in July 2014. The 28 revised full papers and 3 short papers presented were carefully reviewed and selected from 87 submissions. The papers provide research results on all aspects of rewriting and typed lambda calculi, ranging from theoretical and methodological issues to applications in various contexts. They address a wide variety of topics such as algorithmic aspects, implementation, logic, types, semantics, and programming.

• Formal Verification of an Optimizing Compiler.- Challenges in Satisfiability Modulo Theories.- On a Logical Foundation for Explicit Substitutions.- Intruders with Caps.- Tom: Piggybacking Rewriting on Java.- Rewriting Approximations for Fast Prototyping of Static Analyzers.- Determining Unify-Stable Presentations.- Confluence of Pattern-Based Calculi.- A Simple Proof That Super-Consistency Implies Cut Elimination.- Bottom-Up Rewriting Is Inverse Recognizability Preserving.- Adjunction for Garbage Collection with Application to Graph Rewriting.- Non Strict Confluent Rewrite Systems for Data-Structures with Pointers.- Symbolic Model Checking of Infinite-State Systems Using Narrowing.- Delayed Substitutions.- Innermost-Reachability and Innermost-Joinability Are Decidable for Shallow Term Rewrite Systems.- Termination of Rewriting with Right-Flat Rules.- Abstract Critical Pairs and Confluence of Arbitrary Binary Relations.- On the Completeness of Context-Sensitive Order-Sorted Specifications.- KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis.- Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi.- Proving Termination of Rewrite Systems Using Bounds.- Sequence Unification Through Currying.- The Termination Competition.- Random Descent.- Correctness of Copy in Calculi with Letrec.- A Characterization of Medial as Rewriting Rule.- The Maximum Length of Mu-Reduction in Lambda Mu-Calculus.- On Linear Combinations of ?-Terms.- Satisfying KBO Constraints.- Termination by Quasi-periodic Interpretations.
• (source: Nielsen Book Data)

The 18th International Conference on Rewriting Techniques and Applications, held in Paris, France in June 2007, featured presentations and discussions centering on some of the latest advances in the field. This volume presents the proceedings from that meeting. Papers cover current research on all aspects of rewriting, including applications, foundational issues, frameworks, implementations, and semantics.
(source: Nielsen Book Data)

• Formal Verification of an Optimizing Compiler.- Challenges in Satisfiability Modulo Theories.- On a Logical Foundation for Explicit Substitutions.- Intruders with Caps.- Tom: Piggybacking Rewriting on Java.- Rewriting Approximations for Fast Prototyping of Static Analyzers.- Determining Unify-Stable Presentations.- Confluence of Pattern-Based Calculi.- A Simple Proof That Super-Consistency Implies Cut Elimination.- Bottom-Up Rewriting Is Inverse Recognizability Preserving.- Adjunction for Garbage Collection with Application to Graph Rewriting.- Non Strict Confluent Rewrite Systems for Data-Structures with Pointers.- Symbolic Model Checking of Infinite-State Systems Using Narrowing.- Delayed Substitutions.- Innermost-Reachability and Innermost-Joinability Are Decidable for Shallow Term Rewrite Systems.- Termination of Rewriting with Right-Flat Rules.- Abstract Critical Pairs and Confluence of Arbitrary Binary Relations.- On the Completeness of Context-Sensitive Order-Sorted Specifications.- KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis.- Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi.- Proving Termination of Rewrite Systems Using Bounds.- Sequence Unification Through Currying.- The Termination Competition.- Random Descent.- Correctness of Copy in Calculi with Letrec.- A Characterization of Medial as Rewriting Rule.- The Maximum Length of Mu-Reduction in Lambda Mu-Calculus.- On Linear Combinations of ?-Terms.- Satisfying KBO Constraints.- Termination by Quasi-periodic Interpretations.
• (source: Nielsen Book Data)

The 18th International Conference on Rewriting Techniques and Applications, held in Paris, France in June 2007, featured presentations and discussions centering on some of the latest advances in the field. This volume presents the proceedings from that meeting. Papers cover current research on all aspects of rewriting, including applications, foundational issues, frameworks, implementations, and semantics.
(source: Nielsen Book Data)

This book constitutes the refereed proceedings of the 17th International Conference on Rewriting Techniques and Applications, RTA 2006, held in Seattle, WA, USA in August 2006 within the scope of FLoC 2006, the 2006 Federated Logic Conference. The 23 revised full papers and 4 systems description papers carefully reviewed and selected from 52 initial submissions are presented together with 2 invited talks and a plenary talk of the hosting FLoC conference. The papers are organized in topical sections on constraints and optimization, equational reasoning, system verification, lambda calculus, theorem proving, system descriptions, termination, and higher-order rewriting and unification.
(source: Nielsen Book Data)

• Termination Analysis of the Untyped ?-Calculus.- A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems.- Termination of S-Expression Rewriting Systems: Lexicographic Path Ordering for Higher-Order Terms.- Monadic Second-Order Unification Is NP-Complete.- A Certified AC Matching Algorithm.- Matchbox: A Tool for Match-Bounded String Rewriting.- TORPA: Termination of Rewriting Proved Automatically.- Querying Unranked Trees with Stepwise Tree Automata.- A Verification Technique Using Term Rewriting Systems and Abstract Interpretation.- Rewriting for Fitch Style Natural Deductions.- Efficient ?-Evaluation with Interaction Nets.- Proving Properties of Term Rewrite Systems via Logic Programs.- On the Modularity of Confluence in Infinitary Term Rewriting.- mu-term: A Tool for Proving Termination of Context-Sensitive Rewriting.- Automated Termination Proofs with AProVE.- An Approximation Based Approach to Infinitary Lambda Calculi.- Boehm-Like Trees for Term Rewriting Systems.- Dependency Pairs Revisited.- Inductive Theorems for Higher-Order Rewriting.- The Joinability and Unification Problems for Confluent Semi-constructor TRSs.- A Visual Environment for Developing Context-Sensitive Term Rewriting Systems.
• (source: Nielsen Book Data)

This volume contains the proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA 2004), which was held June 2- 5, 2004, at the RWTH Aachen in Germany. RTA is the major forum for the presentation of research on all aspects of rewriting. Previous RTA conferences took place in Dijon (1985), Bordeaux (1987), Chapel Hill (1989), Como (1991), Montreal (1993), Kaiserslautern (1995), Rutgers (1996), Sitges (1997), Tsukuba (1998), Trento (1999), Norwich (2000), Utrecht (2001), Copenhagen (2002), and Valencia (2003). The program committee selected 19 papers for presentation, including ?ve system descriptions, from a total of 43 submissions. In addition, there were invited talks by Neil Jones, Aart Middeldorp, and Robin Milner. Many people helped to make RTA 2004 a success. I am grateful to the m- bers of the program committee and the external referees for reviewing the s- missionsandmaintainingthehighstandardsoftheRTAconferences. Itisagreat pleasure to thank the conference chair Jurgen .. Giesl and the other members of the local organizing committee. They were in charge of the local organization of all events partaking in the Federated Conference on Rewriting, Deduction, and Programming (RDP). Apart from RTA 2004, these events were: - 2nd International Workshop on Higher-Order Rewriting (Delia Kesner, Femke van Raamsdonk, and Joe Wells), - 5th International Workshop on Rule-Based Programming (Slim Abdennadher and Christophe Ringeissen), - 13thInternationalWorkshoponFunctionaland(Constraint)LogicProgr- ming (Herbert Kuchen), - IFIP Working Group 1.
(source: Nielsen Book Data)

• Invited Talk
• Symbolic Systems Biology
• Confluence as a Cut Elimination Property
• Associative-Commutative Rewriting on Large Terms
• A Rule-Based Approach for Automated Generation of Kinetic Chemical Mechanisms
• Efficient Reductions with Director Strings
• Rewriting Logic and Probabilities
• The Maude 2.0 System
• Diagrams for Meaning Preservation
• Expression Reduction Systems with Patterns
• Residuals in Higher-Order Rewriting
• Rewriting UNITY
• New Decidability Results for Fragments of First-Order Logic and Application to Cryptographic Protocols
• An E-unification Algorithm for Analyzing Protocols That Use Modular Exponentiation
• Two-Way Equational Tree Automata for AC-Like Theories: Decidability and Closure Properties
• Rule-Based Analysis of Dimensional Safety
• Invited Talk
• Topological Collections, Transformations and Their Application to the Modeling and the Simulation of Dynamical Systems
• On the Complexity of Higher-Order Matching in the Linear?-Calculus
• XML Schema, Tree Logic and Sheaves Automata
• Size-Change Termination for Term Rewriting
• Monotonic AC-Compatible Semantic Path Orderings
• Relating Derivation Lengths with the Slow-Growing Hierarchy Directly
• Tsukuba Termination Tool
• Liveness in Rewriting
• Validation of the JavaCard Platform with Implicit Induction Techniques
• "Term Partition" for Mathematical Induction
• Equational Prover of Theorema
• Termination of Simply Typed Term Rewriting by Translation and Labelling
• Rewriting Modulo in Deduction Modulo
• Termination of String Rewriting Rules That Have One Pair of Overlaps
• Environments for Term Rewriting Engines for Free!
• Joint RTA-TLCA Invited Talk
• A Logical Algorithm for ML Type Inference
• A Rewriting Alternative to Reidemeister-Schreier
• Stable Computational Semantics of Conflict-Free Rewrite Systems (Partial Orders with Duplication)
• Recognizing Boolean Closed A-Tree Languages with Membership Conditional Rewriting Mechanism
• Testing Extended Regular Language Membership Incrementally by Rewriting.

This book constitutes the refereed proceedings of the 14th International Conference on Rewriting Techniques and Applications, RTA 2003, held in Valencia, Spain in June 2003. The 26 revised regular papers and 6 system descriptions presented together with 3 invited contributions were carefully reviewed and selected from 61 submissions. All current aspects of rewriting are addressed.

• Invited Talks
• Combining Shostak Theories
• Multiset Rewriting and Security Protocol Analysis
• Engineering of Logics for the Content-Based Representation of Information
• Regular Papers, Application Papers
• Axiomatic Rewriting Theory VI: Residual Theory Revisited
• Static Analysis of Modularity of?-Reduction in the Hyperbalanced?-Calculus
• Exceptions in the Rewriting Calculus
• Deriving Focused Lattice Calculi
• Layered Transducing Term Rewriting System and Its Recognizability Preserving Property
• Decidability and Closure Properties of Equational Tree Languages
• Regular Sets of Descendants by Some Rewrite Strategies
• Rewrite Games
• An Extensional Böhm Model
• A Weak Calculus with Explicit Operators for Pattern Matching and Substitution
• Tradeoffs in the Intensional Representation of Lambda Terms
• Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae
• Conditions for Efficiency Improvement by Tree Transducer Composition
• Rewriting Strategies for Instruction Selection
• Probabilistic Rewrite Strategies. Applications to ELAN
• Loops of Superexponential Lengths in One-Rule String Rewriting
• Recursive Derivational Length Bounds for Confluent Term Rewrite Systems Research Paper
• Termination of (Canonical) Context-Sensitive Rewriting
• Atomic Set Constraints with Projection
• Currying Second-Order Unification Problems
• A Decidable Variant of Higher Order Matching
• Combining Decision Procedures for Positive Theories Sharing Constructors
• System Descriptions
• JITty: A Rewriter with Strategy Annotations
• Autowrite: A Tool for Checking Properties of Term Rewriting Systems
• TTSLI: An Implementation of Tree-Tuple Synchronized Languages
• in2: A Graphical Interpreter for Interaction Nets.

This book constitutes the refereed proceedings of the 13th International Conference on Rewriting Techniques and Applications, RTA 2002, held in Copenhagen, Denmark, in July 2002. The 20 regular papers, two application papers, and four system descriptions presented together with three invited contributions were carefully reviewed and selected from 49 submissions. All current aspects of rewriting are addressed.

• Invited Talks.- Computing and Proving.- Rewriting for Deduction and Verification.- Regular Papers.- Universal Interaction Systems with Only Two Agents.- General Recursion on Second Order Term Algebras.- Beta Reduction Constraints.- From Higher-Order to First-Order Rewriting.- Combining Pattern E-Unification Algorithms.- Matching Power.- Dependency Pairs for Equational Rewriting.- Termination Proofs by Context-Dependent Interpretations.- Uniform Normalisation beyond Orthogonality.- Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order.- Relating Accumulative and Non-accumulative Functional Programs.- Context Unification and Traversal Equations.- Weakly Regular Relations and Applications.- On the Parallel Complexity of Tree Automata.- Transfinite Rewriting Semantics for Term Rewriting Systems.- Goal-Directed E-Unification.- The Unification Problem for Confluent Right-Ground Term Rewriting Systems.- On Termination of Higher-Order Rewriting.- Matching with Free Function Symbols - A Simple Extension of Matching?.- Deriving Focused Calculi for Transitive Relations.- A Formalised First-Order Con uence Proof for the ?-Calculus Using One-Sorted Variable Names (Barendregt Was Right after all ... almost).- A Normal Form for Church-Rosser Language Systems.- Confluence and Termination of Simply Typed Term Rewriting Systems.- Parallel Evaluation of Interaction Nets with MPINE.- Stratego: A Language for Program Transformation Based on Rewriting Strategies System Description of Stratego 0.5.
• (source: Nielsen Book Data)

This book constitutes the refereed proceedings of the 12th International Conference on Rewriting Techniques and Applications, RTA 2001, held in Utrecht, The Netherlands, in May 2001. The 23 revised full papers presented together with two system descriptions were carefully reviewed and selected from 55 submissions. All current aspects of rewriting are addressed.
(source: Nielsen Book Data)

• Rewrite techniques in theorem proving
• Redundancy criteria for constrained completion
• Bi-rewriting, a term rewriting technique for monotonic order relations
• A case study of completion modulo distributivity and Abelian groups
• A semantic approach to order-sorted rewriting
• Distributing equational theorem proving
• On the correctness of a distributed memory Gröbner basis algorithm
• Improving transformation systems for general E-unification
• Equational and membership constraints for infinite trees
• Regular path expressions in feature logic
• Proving properties of typed lambda terms: Realizability, covers, and sheaves
• Some lambda calculi with categorical sums and products
• Paths, computations and labels in the?-calculus
• Confluence and superdevelopments
• Relating graph and term rewriting via Böhm models
• Topics in termination
• Total termination of term rewriting
• Simple termination is difficult
• Optimal normalization in orthogonal term rewriting systems
• A graph reduction approach to incremental term rewriting
• Generating tables for bottom-up matching
• On some algorithmic problems for groups and monoids
• Combination techniques and decision problems for disunification
• The negation elimination from syntactic equational formula is decidable
• Encompassment properties and automata with constraints
• Recursively defined tree transductions
• AC complement problems: Satisfiability and negation elimination
• A precedence-based total AC-compatible ordering
• Extension of the associative path ordering to a chain of associative commutative symbols
• Polynomial time termination and constraint satisfaction tests
• Linear interpretations by counting patterns
• Some undecidable termination problems for semi-Thue systems
• Saturation of first-order (constrained) clauses with the Saturate system
• MERILL: An equational reasoning system in standard ML
• Reduce the redex? ReDuX
• Agg
• An implementation of algebraic graph rewriting
• Smaran: A congruence-closure based system for equational computations
• LAMBDALG: Higher order algebraic specification language
• More problems in rewriting.

This volume contains the proceedings of RTA-93, the Fifth International Conference on Rewriting Techniques and Applications, held in Montreal, Canada, in June 1993. The volume includes three invited lectures, "Rewrite Techniques in Theorem Proving" (L. Bachmair); "Proving Properties of Typed Lambda Terms: Realizability, Covers, and Sheaves", (J. Gallier); and "On Some Algorithmic Problems for Groups and Monoids", (S.J. Adian). It also features full versions of 29 papers selected from 91 submissions, 6 system descriptions, and a list of open problems in the field. The papers cover many topics: term rewriting; termination; graph rewriting; constraint solving; semantic unification, disunification and combination; higher-order logics; and theorem proving, with several papers on distributed theorem proving, theorem proving with constraints and completion.
(source: Nielsen Book Data)

• Confluent Term Rewriting Systems.- Generalized Innermost Rewriting.- Orderings for Innermost Termination.- Leanest Quasi-orderings.- Abstract Modularity.- Union of Equational Theories: An Algebraic Approach.- Equivariant Unification.- Faster Basic Syntactic Mutation with Sorts for Some Separable Equational Theories.- Unification in a Class of Permutative Theories.- Dependency Pairs for Simply Typed Term Rewriting.- Universal Algebra for Termination of Higher-Order Rewriting.- Quasi-interpretations and Small Space Bounds.- A Sufficient Completeness Reasoning Tool for Partial Specifications.- Tyrolean Termination Tool.- Call-by-Value Is Dual to Call-by-Name - Reloaded.- ??-Calculus and Duality: Call-by-Name and Call-by-Value.- Reduction in a Linear Lambda-Calculus with Applications to Operational Semantics.- Higher-Order Matching in the Linear Lambda Calculus in the Absence of Constants Is NP-Complete.- Localized Fairness: A Rewriting Semantics.- Partial Inversion of Constructor Term Rewriting Systems.- Natural Narrowing for General Term Rewriting Systems.- The Finite Variant Property: How to Get Rid of Some Algebraic Properties.- Intruder Deduction for AC-Like Equational Theories with Homomorphisms.- Proving Positive Almost-Sure Termination.- Termination of Single-Threaded One-Rule Semi-Thue Systems.- On Tree Automata that Certify Termination of Left-Linear Term Rewriting Systems.- Twenty Years Later.- Open. Closed. Open..- A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code.- Extending the Explicit Substitution Paradigm.- Arithmetic as a Theory Modulo.- Infinitary Combinatory Reduction Systems.- Proof-Producing Congruence Closure.- The Algebra of Equality Proofs.- On Computing Reachability Sets of Process Rewrite Systems.- Automata and Logics for Unranked and Unordered Trees.
• (source: Nielsen Book Data)

This volume contains the proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA2005), whichwasheldonApril19- 21, 2005, at the Nara-Ken New Public Hall in the center of the Nara National Park in Nara, Japan. RTA is the major forum for the presentation of research on all aspects of rewriting.PreviousRTAconferenceswereheldinDijon(1985), Bordeaux(1987), Chapel Hill (1989), Como (1991), Montreal (1993), Kaiserslautern (1995), Rutgers (1996), Sitges (1997), Tsukuba (1998), Trento (1999), Norwich (2000), Utrecht (2001), Copenhagen (2002), Valencia (2003), and Aachen (2004). This year, there were 79 submissions from 20 countries, of which 31 papers were accepted for publication (29 regular papers and 2 system descriptions). The submissions came from France (10 accepted papers of the 23.1 submitted papers), USA (5.6 of 11.7), Japan (4 of 9), Spain (2.7 of 6.5), UK (2.7 of 4.7), The Netherlands (1.7 of 3.8), Germany (1.3 of 2.3), Austria (1 of 1), Poland (1 of 1), Israel (0.5 of 0.8), Denmark (0.5 of 0.5), China (0 of 4), Korea (0 of 4), Taiwan (0 of 1.3), Australia (0 of 1), Brazil (0 of 1), Russia (0 of 1), Switzerland (0 of 1), Sweden (0 of 1), and Italy (0 of 0.3). Each submission was assigned to at least three Program Committee m- bers, who carefully reviewed the papers, with the help of 111 external referees.
(source: Nielsen Book Data)

• Confluent Term Rewriting Systems.- Generalized Innermost Rewriting.- Orderings for Innermost Termination.- Leanest Quasi-orderings.- Abstract Modularity.- Union of Equational Theories: An Algebraic Approach.- Equivariant Unification.- Faster Basic Syntactic Mutation with Sorts for Some Separable Equational Theories.- Unification in a Class of Permutative Theories.- Dependency Pairs for Simply Typed Term Rewriting.- Universal Algebra for Termination of Higher-Order Rewriting.- Quasi-interpretations and Small Space Bounds.- A Sufficient Completeness Reasoning Tool for Partial Specifications.- Tyrolean Termination Tool.- Call-by-Value Is Dual to Call-by-Name - Reloaded.- ??-Calculus and Duality: Call-by-Name and Call-by-Value.- Reduction in a Linear Lambda-Calculus with Applications to Operational Semantics.- Higher-Order Matching in the Linear Lambda Calculus in the Absence of Constants Is NP-Complete.- Localized Fairness: A Rewriting Semantics.- Partial Inversion of Constructor Term Rewriting Systems.- Natural Narrowing for General Term Rewriting Systems.- The Finite Variant Property: How to Get Rid of Some Algebraic Properties.- Intruder Deduction for AC-Like Equational Theories with Homomorphisms.- Proving Positive Almost-Sure Termination.- Termination of Single-Threaded One-Rule Semi-Thue Systems.- On Tree Automata that Certify Termination of Left-Linear Term Rewriting Systems.- Twenty Years Later.- Open. Closed. Open..- A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code.- Extending the Explicit Substitution Paradigm.- Arithmetic as a Theory Modulo.- Infinitary Combinatory Reduction Systems.- Proof-Producing Congruence Closure.- The Algebra of Equality Proofs.- On Computing Reachability Sets of Process Rewrite Systems.- Automata and Logics for Unranked and Unordered Trees.
• (source: Nielsen Book Data)

This volume contains the proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA2005), whichwasheldonApril19- 21, 2005, at the Nara-Ken New Public Hall in the center of the Nara National Park in Nara, Japan. RTA is the major forum for the presentation of research on all aspects of rewriting.PreviousRTAconferenceswereheldinDijon(1985), Bordeaux(1987), Chapel Hill (1989), Como (1991), Montreal (1993), Kaiserslautern (1995), Rutgers (1996), Sitges (1997), Tsukuba (1998), Trento (1999), Norwich (2000), Utrecht (2001), Copenhagen (2002), Valencia (2003), and Aachen (2004). This year, there were 79 submissions from 20 countries, of which 31 papers were accepted for publication (29 regular papers and 2 system descriptions). The submissions came from France (10 accepted papers of the 23.1 submitted papers), USA (5.6 of 11.7), Japan (4 of 9), Spain (2.7 of 6.5), UK (2.7 of 4.7), The Netherlands (1.7 of 3.8), Germany (1.3 of 2.3), Austria (1 of 1), Poland (1 of 1), Israel (0.5 of 0.8), Denmark (0.5 of 0.5), China (0 of 4), Korea (0 of 4), Taiwan (0 of 1.3), Australia (0 of 1), Brazil (0 of 1), Russia (0 of 1), Switzerland (0 of 1), Sweden (0 of 1), and Italy (0 of 0.3). Each submission was assigned to at least three Program Committee m- bers, who carefully reviewed the papers, with the help of 111 external referees.
(source: Nielsen Book Data)

• Origin tracking in term rewriting.- Simultaneous critical pairs and Church-Rosser property.- Church-Rosser theorems for abstract reduction modulo an equivalence relation.- Automatic monoids versus monoids with finite convergent presentations.- Decidable and undecidable second-order unification problems.- On the exponent of periodicity of minimal solutions of context equations.- Unification in extensions of shallow equational theories.- Unification and matching in process algebras.- E-unification for subsystems of S4.- Solving disequations modulo some class of rewrite systems.- About proofs by consistency.- Normalization of S-terms is decidable.- Decidable approximations of sets of descendants and sets of normal forms.- Algorithms and reductions for rewriting problems.- The decidability of simultaneous rigid E-unification with one variable.- Ordering constraints over feature trees expressed in second-order monadic logic.- Co-definite set constraints.- Modularity of termination using dependency pairs.- Termination of associative-commutative rewriting by dependency pairs.- Termination transformation by tree lifting ordering.- Towards automated termination proofs through "freezing".- Higher-order rewriting and partial evaluation.- SN combinators and partial combinatory algebras.- Coupling saturation-based provers by exchanging positive/negative information.- An on-line problem database.
• (source: Nielsen Book Data)

This book constitutes the refereed proceedings of the 9th International Conference on Rewriting Techniques and Applications, RTA-98, held in Tsukuba, Japan, in March/April 1998. The 22 revised full papers presented were carefully selected from a total of 61 submissions by the program committee with the assistance of 113 additional referees. The book covers all current aspects of rewriting including rewriting systems, term rewriting, string rewriting, theorem proving, resolution, normalization, unification, equational logics, lambda calculus, constraint solving, and functional programming.
(source: Nielsen Book Data)

• Automatic Termination
• Loops under Strategies
• Proving Termination of Integer Term Rewriting
• Dependency Pairs and Polynomial Path Orders
• Unique Normalization for Shallow TRS
• The Existential Fragment of the One-Step Parallel Rewriting Theory
• Proving Confluence of Term Rewriting Systems Automatically
• A Proof Theoretic Analysis of Intruder Theories
• Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case
• Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions
• YAPA: A Generic Tool for Computing Intruder Knowledge
• Well-Definedness of Streams by Termination
• Modularity of Convergence in Infinitary Rewriting
• A Heterogeneous Pushout Approach to Term-Graph Transformation
• An Explicit Framework for Interaction Nets
• Dual Calculus with Inductive and Coinductive Types
• Comparing Böhm-Like Trees
• The Derivational Complexity Induced by the Dependency Pair Method
• Local Termination
• VMTL-A Modular Termination Laboratory
• Tyrolean Termination Tool 2
• From Outermost to Context-Sensitive Rewriting
• A Fully Abstract Semantics for Constructor Systems
• The -Completeness of Most of the Properties of Rewriting Systems You Care About (and Productivity)
• Unification in the Description Logic
• Unification with Singleton Tree Grammars
• Unification and Narrowing in Maude 2.4.

This book constitutes the refereed proceedings of the 20th International Conference on Rewriting Techniques and Applications, RTA 2009, held in Brasilia, Brazil, during June 29 - July 1, 2009. The 22 revised full papers and four system descriptions presented were carefully reviewed and selected from 59 initial submissions. The papers cover current research on all aspects of rewriting including typical areas of interest such as applications, foundational issues, frameworks, implementations and semantics.
(source: Nielsen Book Data)

This book constitutes the refereed proceedings of the 19th International Conference on Rewriting Techniques and Applications, RTA 2008, held in Hagenberg, Austria, July 15-17, in June 2008 as part of the RISC Summer 2008. The 30 revised full papers presented were carefully reviewed and selected from 57 initial submissions. The papers cover current research on all aspects of rewriting including typical areas of interest such as applications, foundational issues, frameworks, implementations, and semantics.
(source: Nielsen Book Data)

• Term rewriting and universal algebra in historical perspective.- Characterizations of unification type zero.- Proof normalization for resolution and paramodulation.- Complete sets of reductions modulo associativity, commutativity and identity.- Completion-time optimization of rewrite-time goal solving.- Computing ground reducibility and inductively complete positions.- Inductive proofs by specification transformations.- Narrowing and unification in functional programming -An evaluation mechanism for absolute set abstraction.- Simulation of Turing machines by a left-linear rewrite rule.- Higher-order unification with dependent function types.- An overview of LP, the Larch Prover.- Graph grammars, a new paradigm for implementing visual languages.- Termination proofs and the length of derivations.- Abstract rewriting with concrete operators.- On how to move mountains `associatively and commutatively'.- Generalized Groebner bases: Theory and applications. A condensation.- A local termination property for term rewriting systems.- An equational logic sampler.- Modular aspects of properties of term rewriting systems related to normal forms.- Priority rewriting: Semantics, confluence, and conditionals.- Negation with logical variables in conditional rewriting.- Algebraic semantics and complexity of term rewriting systems.- Optimization by non-deterministic, lazy rewriting.- Combining matching algorithms: The regular case.- Restrictions of congruences generated by finite canonical string-rewriting systems.- Embedding with patterns and associated recursive path ordering.- Rewriting techniques for program synthesis.- Transforming strongly sequential rewrite systems with constructors for efficient parallel execution.- Efficient ground completion.- Extensions and comparison of simplification orderings.- Classes of equational programs that compile into efficient machine code.- Fair termination is decidable for ground systems.- Termination for the direct sum of left-linear term rewriting systems.- Conditional rewrite rule systems with built-in arithmetic and induction.- Consider only general superpositions in completion procedures.- Solving systems of linear diophantine equations and word equations.- SbRev
• e2: A term rewriting laboratory with (AC)-unfailing completion.- THEOPOGLES - An efficient theorem prover based on rewrite-techniques.- Comtes - An experimental environment for the completion of term rewriting systems.- Asspegique: An integrated specification environment.- KBlab: An equational theorem prover for the Macintosh.- Fast Knuth-Bendix completion: Summary.- Compilation of ground term rewriting systems and applications (DEMO).- An overview of Rewrite Rule Laboratory (RRL).- InvX: An automatic function inverter.- A parallel implementation of rewriting and narrowing.- Morphocompletion for one-relation monoids.
• (source: Nielsen Book Data)

Rewriting has always played an important role in symbolic manipulation and automated deduction systems. The theory of rewriting is an outgrowth of Combinatory Logic and the Lambda Calculus. Applications cover broad areas in automated reasoning, programming language design, semantics, and implementations, and symbolic and algebraic manipulation. The proceedings of the third International Conference on Rewriting Techniques and Applications contain 34 regular papers, covering many diverse aspects of rewriting (including equational logic, decidability questions, term rewriting, congruence-class rewriting, string rewriting, conditional rewriting, graph rewriting, functional and logic programming languages, lazy and parallel implementations, termination issues, compilation techniques, completion procedures, unification and matching algorithms, deductive and inductive theorem proving, Groebner bases, and program synthesis). It also contains 12 descriptions of implemented equational reasoning systems. Anyone interested in the latest advances in this fast growing area should read this volume.
(source: Nielsen Book Data)

This book constitutes the refereed proceedings of the 11th International Conference on Rewriting Techniques and Applications, RTA 2000, held in Norwich, UK, in July 2000.The 15 revised full papers and three system descriptions presented together with two invited contributions were carefully reviewed and selected from 44 submissions. All current aspects of rewriting are addressed.
(source: Nielsen Book Data)