000 04975nam a22006015i 4500
001 978-3-319-08918-8
003 DE-He213
005 20240730182045.0
007 cr nn 008mamaa
008 140701s2014 sz | s |||| 0|eng d
020 _a9783319089188
_9978-3-319-08918-8
024 7 _a10.1007/978-3-319-08918-8
_2doi
050 4 _aQA267-268.5
072 7 _aUYA
_2bicssc
072 7 _aCOM014000
_2bisacsh
072 7 _aUYA
_2thema
082 0 4 _a005.131
_223
245 1 0 _aRewriting and Typed Lambda Calculi
_h[electronic resource] :
_bJoint International Conferences, RTA and TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings /
_cedited by Gilles Dowek.
250 _a1st ed. 2014.
264 1 _aCham :
_bSpringer International Publishing :
_bImprint: Springer,
_c2014.
300 _aXXII, 491 p. 58 illus.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aTheoretical Computer Science and General Issues,
_x2512-2029 ;
_v8560
505 0 _aProcess 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.
520 _aThis 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.
650 0 _aMachine theory.
_9127099
650 0 _aComputer science
_xMathematics.
_93866
650 0 _aComputer science.
_99832
650 0 _aArtificial intelligence.
_93407
650 0 _aMathematical logic.
_92258
650 1 4 _aFormal Languages and Automata Theory.
_9127100
650 2 4 _aMathematics of Computing.
_931875
650 2 4 _aComputer Science Logic and Foundations of Programming.
_942203
650 2 4 _aSymbolic and Algebraic Manipulation.
_955589
650 2 4 _aArtificial Intelligence.
_93407
650 2 4 _aMathematical Logic and Foundations.
_934712
700 1 _aDowek, Gilles.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9127101
710 2 _aSpringerLink (Online service)
_9127102
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783319089171
776 0 8 _iPrinted edition:
_z9783319089195
830 0 _aTheoretical Computer Science and General Issues,
_x2512-2029 ;
_v8560
_9127103
856 4 0 _uhttps://doi.org/10.1007/978-3-319-08918-8
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cELN
999 _c91208
_d91208