Computer Science Logic: 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings (Lecture Notes in Computer Science)

This book constitutes the refereed proceedings of the 18th International Workshop on Computer Science Logic, CSL 2004, held as the 13th Annual Conference of the EACSL in Karpacz, Poland, in September 2004. The 33 revised full papers presented together with 5 invited contributions were carefully reviewed and selected from 88 papers submitted. All current aspects of logic in computer science are addressed ranging from mathematical logic and logical foundations to methodological issues and applications of logics in various computing contexts. Thisvolumecontainspapersselectedforpresentationatthe2004annualconf- 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. Invited 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. Jerzy Marcinkowski, Andrzej Tarlecki (eds.). Includes Bibliographical References And Index. Front Matter....Pages - Notions of Average-Case Complexity for Random 3-SAT....Pages 1-5 Abstract Interpretation of Proofs: Classical Propositional Calculus....Pages 6-21 Applications of Craig Interpolation to Model Checking....Pages 22-23 Bindings, Mobility of Bindings, and the ∇-Quantifier: An Abstract....Pages 24-24 My (Un)Favourite Things....Pages 25-25 On Nash Equilibria in Stochastic Games....Pages 26-40 A Bounding Quantifier....Pages 41-55 Parity and Exploration Games on Infinite Graphs....Pages 56-70 Integrating Equational Reasoning into Instantiation-Based Theorem Proving....Pages 71-84 Goal-Directed Methods for Łukasiewicz Logic....Pages 85-99 A General Theorem on Termination of Rewriting....Pages 100-114 Predicate Transformers and Linear Logic: Yet Another Denotational Model....Pages 115-129 Structures for Multiplicative Cyclic Linear Logic: Deepness vs Cyclicity....Pages 130-144 On Proof Nets for Multiplicative Linear Logic with Units....Pages 145-159 The Boundary Between Decidability and Undecidability for Transitive-Closure Logics....Pages 160-174 Game-Based Notions of Locality Over Finite Models....Pages 175-189 Fixed Points of Type Constructors and Primitive Recursion....Pages 190-204 On the Building of Affine Retractions....Pages 205-219 Higher-Order Matching in the Linear λ -calculus with Pairing....Pages 220-234 A Dependent Type Theory with Names and Binding....Pages 235-249 Towards Mechanized Program Verification with Separation Logic....Pages 250-264 A Functional Scenario for Bytecode Verification of Resource Bounds....Pages 265-279 Proving Abstract Non-interference....Pages 280-294 Intuitionistic LTL and a New Characterization of Safety and Liveness....Pages 295-309 Moving in a Crumbling Network: The Balanced Case....Pages 310-324 Parameterized Model Checking of Ring-Based Message Passing Systems....Pages 325-339 A Third-Order Bounded Arithmetic Theory for PSPACE....Pages 340-354 Provably Total Primitive Recursive Functions: Theories with Induction....Pages 355-369 Logical Characterizations of PSPACE....Pages 370-384 The Logic of the Partial λ -Calculus with Equality....Pages 385-399 Complete Lax Logical Relations for Cryptographic Lambda-Calculi....Pages 400-414 Subtyping Union Types....Pages 415-429 Pfaffian Hybrid Systems....Pages 430-441 Axioms for Delimited Continuations in the CPS Hierarchy....Pages 442-457 Set Constraints on Regular Terms....Pages 458-472 Unsound Theorem Proving....Pages 473-487 A Space Efficient Implementation of a Tableau Calculus for a Logic with a Constructive Negation....Pages 488-502 Automated Generation of Analytic Calculi for Logics with Linearity....Pages 503-517 Back Matter....Pages - Thisvolumecontainspapersselectedforpresentationatthe2004AnnualConf- 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