000 04256nam a22005655i 4500
001 978-3-540-30124-0
003 DE-He213
005 20240423125928.0
007 cr nn 008mamaa
008 121227s2004 gw | s |||| 0|eng d
020 _a9783540301240
_9978-3-540-30124-0
024 7 _a10.1007/b100120
_2doi
050 4 _aQA76.76.C65
072 7 _aUMC
_2bicssc
072 7 _aCOM010000
_2bisacsh
072 7 _aUMC
_2thema
082 0 4 _a005.45
_223
245 1 0 _aComputer Science Logic
_h[electronic resource] :
_b18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings /
_cedited by Jerzy Marcinkowski.
250 _a1st ed. 2004.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg :
_bImprint: Springer,
_c2004.
300 _aXI, 522 p.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aLecture Notes in Computer Science,
_x1611-3349 ;
_v3210
505 0 _aInvited Lectures -- Notions of Average-Case Complexity for Random 3-SAT -- Abstract Interpretation of Proofs: Classical Propositional Calculus -- Applications of Craig Interpolation to Model Checking -- Bindings, Mobility of Bindings, and the ?-Quantifier: An Abstract -- My (Un)Favourite Things -- Regular Papers -- On Nash Equilibria in Stochastic Games -- A Bounding Quantifier -- Parity and Exploration Games on Infinite Graphs -- Integrating Equational Reasoning into Instantiation-Based Theorem Proving -- Goal-Directed Methods for ?ukasiewicz Logic -- A General Theorem on Termination of Rewriting -- Predicate Transformers and Linear Logic: Yet Another Denotational Model -- Structures for Multiplicative Cyclic Linear Logic: Deepness vs Cyclicity -- On Proof Nets for Multiplicative Linear Logic with Units -- The Boundary Between Decidability and Undecidability for Transitive-Closure Logics -- Game-Based Notions of Locality Over Finite Models -- Fixed Points of Type Constructors and Primitive Recursion -- On the Building of Affine Retractions -- Higher-Order Matching in the Linear ?-calculus with Pairing -- A Dependent Type Theory with Names and Binding -- Towards Mechanized Program Verification with Separation Logic -- A Functional Scenario for Bytecode Verification of Resource Bounds -- Proving Abstract Non-interference -- Intuitionistic LTL and a New Characterization of Safety and Liveness -- Moving in a Crumbling Network: The Balanced Case -- Parameterized Model Checking of Ring-Based Message Passing Systems -- A Third-Order Bounded Arithmetic Theory for PSPACE -- Provably Total Primitive Recursive Functions: Theories with Induction -- Logical Characterizations of PSPACE -- The Logic of the Partial ?-Calculus with Equality -- Complete Lax Logical Relations for Cryptographic Lambda-Calculi.-Subtyping Union Types -- Pfaffian Hybrid Systems -- Axioms for Delimited Continuations in the CPS Hierarchy -- Set Constraints on Regular Terms -- Unsound Theorem Proving -- A Space Efficient Implementation of a Tableau Calculus for a Logic with a Constructive Negation -- Automated Generation of Analytic Calculi for Logics with Linearity.
650 0 _aCompilers (Computer programs).
650 0 _aMachine theory.
650 0 _aArtificial intelligence.
650 0 _aComputer science.
650 1 4 _aCompilers and Interpreters.
650 2 4 _aFormal Languages and Automata Theory.
650 2 4 _aArtificial Intelligence.
650 2 4 _aComputer Science Logic and Foundations of Programming.
700 1 _aMarcinkowski, Jerzy.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
710 2 _aSpringerLink (Online service)
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783540230243
776 0 8 _iPrinted edition:
_z9783662164976
830 0 _aLecture Notes in Computer Science,
_x1611-3349 ;
_v3210
856 4 0 _uhttps://doi.org/10.1007/b100120
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
912 _aZDB-2-BAE
942 _cSPRINGER
999 _c183197
_d183197