Term Rewriting and Applications 17th International Conference, RTA 2006 Seattle, WA, USA, August 12-14, 2006 Proceedings /
Συγγραφή απο Οργανισμό/Αρχή: | |
---|---|
Άλλοι συγγραφείς: | |
Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
Γλώσσα: | English |
Έκδοση: |
Berlin, Heidelberg :
Springer Berlin Heidelberg,
2006.
|
Σειρά: | Lecture Notes in Computer Science,
4098 |
Θέματα: | |
Διαθέσιμο Online: | Full Text via HEAL-Link |
Πίνακας περιεχομένων:
- FLoC Plenary Talk
- Formal Verification of Infinite State Systems Using Boolean Methods
- Session 1. Constraints and Optimization
- Solving Partial Order Constraints for LPO Termination
- Computationally Equivalent Elimination of Conditions
- On the Correctness of Bubbling
- Propositional Tree Automata
- Session 2. Equational Reasoning
- Generalizing Newman’s Lemma for Left-Linear Rewrite Systems
- Unions of Equational Monadic Theories
- Modular Church-Rosser Modulo
- Session 3. System Verification
- Hierarchical Combination of Intruder Theories
- Feasible Trace Reconstruction for Rewriting Approximations
- Invited Talk
- Rewriting Models of Boolean Programs
- Session 4. Lambda Calculus
- Syntactic Descriptions: A Type System for Solving Matching Equations in the Linear ?-Calculus
- A Terminating and Confluent Linear Lambda Calculus
- A Lambda-Calculus with Constructors
- Structural Proof Theory as Rewriting
- Session 5. Theorem Proving
- Checking Conservativity of Overloaded Definitions in Higher-Order Logic
- Certified Higher-Order Recursive Path Ordering
- Dealing with Non-orientable Equations in Rewriting Induction
- Session 6. System Descriptions
- TPA: Termination Proved Automatically
- RAPT: A Program Transformation System Based on Term Rewriting
- The CL-Atse Protocol Analyser
- Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
- Invited Talk
- Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
- Session 7. Termination
- Predictive Labeling
- Termination of String Rewriting with Matrix Interpretations
- Decidability of Termination for Semi-constructor TRSs, Left-Linear Shallow TRSs and Related Systems
- Proving Positive Almost Sure Termination Under Strategies
- Session 8. Higher-Order Rewriting and Unification
- A Proof of Finite Family Developments for Higher-Order Rewriting Using a Prefix Property
- Higher-Order Orderings for Normal Rewriting
- Bounded Second-Order Unification Is NP-Complete.