Rewriting and Typed Lambda Calculi Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Dowek, Gilles (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Cham : Springer International Publishing : Imprint: Springer, 2014.
• Σειρά: Lecture Notes in Computer Science, 8560
• Θέματα: Computer science.; Computer logic.; Mathematical logic.; Computer science > Mathematics.; Computers.; Computer Science.; Mathematical Logic and Formal Languages.; Mathematics of Computing.; Logics and Meanings of Programs.; Symbolic and Algebraic Manipulation.; Computing Methodologies.; Mathematical Logic and Foundations.

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

Πίνακας περιεχομένων:

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