Computer Science Logic: 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Proceedings

Samson Abramsky (auth.), Jacques Duparc, Thomas A. Henzinger (eds.)3540749144, 9783540749141

This book constitutes the refereed proceedings of the 21st International Workshop on Computer Science Logic, CSL 2007, held as the 16th Annual Conference of the EACSL in Lausanne, Switzerland in September 2007.

The 36 revised full papers presented together with the abstracts of six invited lectures were carefully reviewed and selected from 116 submissions. The papers are organized in topical sections on logic and games, expressiveness, games and trees, logic and deduction, lambda calculus, finite model theory, linear logic, proof theory, and game semantics.

---

Table of contents :
Front Matter….Pages –
Full Completeness: Interactive and Geometric Characterizations of the Space of Proofs (Abstract)….Pages 1-2
The Symbolic Approach to Repeated Games (Abstract)….Pages 3-3
Proofs, Programs and Abstract Complexity….Pages 4-5
Model-Checking First-Order Logic: Automata and Locality….Pages 6-6
Tightening the Exchange Rates Between Automata….Pages 7-22
Precise Relational Invariants Through Strategy Iteration….Pages 23-40
Omega-Regular Half-Positional Winning Conditions….Pages 41-53
Clique-Width and Parity Games….Pages 54-68
Logical Refinements of Church’s Problem….Pages 69-83
The Power of Counting Logics on Restricted Classes of Finite Structures….Pages 84-98
Comparing the Expressive Power of Well-Structured Transition Systems….Pages 99-114
There Exist Some ω -Powers of Any Borel Rank….Pages 115-129
Satisfiability of a Spatial Logic with Tree Variables….Pages 130-145
Forest Expressions….Pages 146-160
MSO on the Infinite Binary Tree: Choice and Order….Pages 161-176
Classical and Intuitionistic Logic Are Asymptotically Identical….Pages 177-193
Qualitative Temporal and Spatial Reasoning Revisited….Pages 194-207
On Acyclic Conjunctive Queries and Constant Delay Enumeration….Pages 208-222
Integrating Linear Arithmetic into Superposition Calculus….Pages 223-237
The Theory of Calculi with Explicit Substitutions Revisited….Pages 238-252
A Soft Type Assignment System for λ -Calculus….Pages 253-267
Lambda Theories of Effective Lambda Models….Pages 268-282
Typed Normal Form Bisimulation….Pages 283-297
Not Enough Points Is Enough….Pages 298-312
Classical Program Extraction in the Calculus of Constructions….Pages 313-327
Building Decision Procedures in the Calculus of Inductive Constructions….Pages 328-342
Structure Theorem and Strict Alternation Hierarchy for FO 2 on Words….Pages 343-357
On the Complexity of Reasoning About Dynamic Policies….Pages 358-373
Relativizing Small Complexity Classes and Their Theories….Pages 374-388
Subexponential Time and Fixed-Parameter Tractability: Exploiting the Miniaturization Mapping….Pages 389-404
From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic….Pages 405-419
Linear Realizability….Pages 420-434
Correctness of Multiplicative (and Exponential) Proof Structures is NL -Complete….Pages 435-450
Focusing and Polarization in Intuitionistic Logic….Pages 451-465
Incorporating Tables into Proofs….Pages 466-480
A Cut-Free and Invariant-Free Sequent Calculus for PLTL ….Pages 481-495
Unbounded Proof-Length Speed-Up in Deduction Modulo….Pages 496-511
Propositional Logic for Circuit Classes….Pages 512-526
Game Characterizations and the PSPACE-Completeness of Tree Resolution Space….Pages 527-541
Continuous Previsions….Pages 542-557
Bad Variables Under Control….Pages 558-572
A Games Model of Bunched Implications….Pages 573-588
The Ackermann Award 2007….Pages 589-597
Back Matter….Pages –