LEADER 06517nam 22006975 450 001 9910767565303321 005 20200630001918.0 010 $a3-540-30124-0 024 7 $a10.1007/b100120 035 $a(CKB)1000000000212527 035 $a(DE-He213)978-3-540-30124-0 035 $a(SSID)ssj0000127880 035 $a(PQKBManifestationID)11137090 035 $a(PQKBTitleCode)TC0000127880 035 $a(PQKBWorkID)10061732 035 $a(PQKB)11289612 035 $a(MiAaPQ)EBC3089032 035 $a(PPN)155216589 035 $a(EXLCZ)991000000000212527 100 $a20121227d2004 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aComputer Science Logic $e18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings /$fedited by Jerzy Marcinkowski 205 $a1st ed. 2004. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2004. 215 $a1 online resource (XI, 522 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v3210 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-23024-6 320 $aIncludes bibliographical references and index. 327 $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. 330 $aThisvolumecontainspapersselectedforpresentationatthe2004AnnualConf- enceoftheEuropeanAssociationforComputerScienceLogic,heldonSeptember 20?24, 2004 in Karpacz, Poland. The CSL conference series started as the International Workshops on C- puterScienceLogic,andthen,after?vemeetings,becametheAnnualConference of the European Association for Computer Science Logic. This conference was the 18th meeting, and the 13th EACSL conference. Altogether 99 abstracts were submitted, followed by 88 papers. Each of these paperswasrefereedbyatleastthreereviewers.Then,afteratwo-weekelectronic discussion, the Programme Committee selected 33 papers for presentation at the conference. Apart from the contributed papers, the Committee invited lectures from Albert Atserias, Martin Hyland, Dale Miller, Ken McMillan and Pawel Urzyczyn. WewouldliketothankallPCmembersandthesubrefereesfortheirexcellent work. The electronic PC meeting would not be possible without good software support. We decided to use the GNU CyberChair system, created by Richard van de Stadt, and we are happy with this decision. We also would like to thank Micha l Moskal who installed and ran CyberChair for us. Finally, we would like to thank ToMasz Wierzbicki, who helped with the preparation of this volume. We gratefully acknowledge ?nancial support for the conference received from the Polish Committee for Scienti?c Research, and Wroc law University. July 2004 Jerzy Marcinkowski and Andrzej Tarlecki Organization CSL 2004 was organized by the Institute of Computer Science, Wrocla w University. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v3210 606 $aProgramming languages (Electronic computers) 606 $aMathematical logic 606 $aArtificial intelligence 606 $aComputer logic 606 $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 615 0$aProgramming languages (Electronic computers). 615 0$aMathematical logic. 615 0$aArtificial intelligence. 615 0$aComputer logic. 615 14$aProgramming Languages, Compilers, Interpreters. 615 24$aMathematical Logic and Formal Languages. 615 24$aArtificial Intelligence. 615 24$aLogics and Meanings of Programs. 676 $a005.1/01/5113 702 $aMarcinkowski$b Jerzy$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910767565303321 996 $aComputer Science Logic$9771972 997 $aUNINA