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

Albert Atserias (auth.), Jerzy Marcinkowski, Andrzej Tarlecki (eds.)3540230246, 9783540230243, 9783540301240

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.

---

Table of contents :
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 –