LEADER 04669nam 22007095 450 001 996465591603316 005 20230406060557.0 010 $a3-540-36835-3 024 7 $a10.1007/11805618 035 $a(CKB)1000000000233062 035 $a(SSID)ssj0000320335 035 $a(PQKBManifestationID)11238877 035 $a(PQKBTitleCode)TC0000320335 035 $a(PQKBWorkID)10348333 035 $a(PQKB)10632372 035 $a(DE-He213)978-3-540-36835-9 035 $a(MiAaPQ)EBC3068187 035 $a(PPN)123137039 035 $a(EXLCZ)991000000000233062 100 $a20100301d2006 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aTerm Rewriting and Applications$b[electronic resource] $e17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings /$fedited by Frank Pfenning 205 $a1st ed. 2006. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2006. 215 $a1 online resource (XIV, 418 p.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v4098 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-36834-5 320 $aIncludes bibliographical references and index. 327 $aFLoC 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. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v4098 606 $aCompilers (Computer programs) 606 $aMachine theory 606 $aComputer science 606 $aArtificial intelligence 606 $aComputer science?Mathematics 606 $aCompilers and Interpreters 606 $aFormal Languages and Automata Theory 606 $aComputer Science Logic and Foundations of Programming 606 $aArtificial Intelligence 606 $aSymbolic and Algebraic Manipulation 615 0$aCompilers (Computer programs). 615 0$aMachine theory. 615 0$aComputer science. 615 0$aArtificial intelligence. 615 0$aComputer science?Mathematics. 615 14$aCompilers and Interpreters. 615 24$aFormal Languages and Automata Theory. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aArtificial Intelligence. 615 24$aSymbolic and Algebraic Manipulation. 676 $a005.131 702 $aPfenning$b Frank$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aInternational Conference on Rewriting Techniques and Applications 906 $aBOOK 912 $a996465591603316 996 $aTerm Rewriting and Applications$9772114 997 $aUNISA