Computer Science Logic: 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005. Proceedings

Maarten Marx (auth.), Luke Ong (eds.)3540282319, 9783540282310

This book constitutes the refereed proceedings of the 19th International Workshop on Computer Science Logic, CSL 2005, held as the 14th Annual Conference of the EACSL in Oxford, UK in August 2005.

The 33 revised full papers presented together with 4 invited contributions were carefully reviewed and selected from 108 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. The volume is organized in topical sections on semantics and logics, type theory and lambda calculus, linear logic and ludics, constraints, finite models, decidability and complexity, verification and model checking, constructive reasoning and computational mathematics, and implicit computational complexity and rewriting.

---

Table of contents :
Front Matter….Pages –
XML Navigation and Tarski’s Relation Algebras….Pages 1-2
Verification in Predicate Logic with Time: Algorithmic Questions….Pages 3-17
Note on Formal Analogical Reasoning in the Juridical Context….Pages 18-26
An Abstract Strong Normalization Theorem….Pages 27-35
On Bunched Polymorphism….Pages 36-50
Distributed Control Flow with Classical Modal Logic….Pages 51-69
A Logic of Coequations….Pages 70-86
A Semantic Formulation of ⊤ ⊤-Lifting and Logical Predicates for Computational Metalanguage….Pages 87-102
Order Structures on Böhm-Like Models….Pages 103-118
Higher-Order Matching and Games….Pages 119-134
Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations….Pages 135-150
On the Role of Type Decorations in the Calculus of Inductive Constructions….Pages 151-166
L-Nets, Strategies and Proof-Nets….Pages 167-183
Permutative Logic….Pages 184-199
Focusing the Inverse Method for Linear Logic….Pages 200-215
Towards a Typed Geometry of Interaction….Pages 216-231
From Pebble Games to Tractability: An Ambidextrous Consistency Algorithm for Quantified Constraint Satisfaction….Pages 232-247
An Algebraic Approach for the Unsatisfiability of Nonlinear Constraints….Pages 248-262
Coprimality in Finite Models….Pages 263-275
Towards a Characterization of Order-Invariant Queries over Tame Structures….Pages 276-291
Decidability of Term Algebras Extending Partial Algebras….Pages 292-308
Results on the Guarded Fragment with Equivalence or Transitive Relations….Pages 309-324
The Modular Decomposition of Countable Graphs: Constructions in Monadic Second-Order Logic….Pages 325-338
On the Complexity of Hybrid Logics with Binders….Pages 339-354
The Complexity of Independence-Friendly Fixpoint Logic….Pages 355-368
Closure Properties of Weak Systems of Bounded Arithmetic….Pages 369-383
Transfinite Extension of the Mu-Calculus….Pages 384-396
Bounded Model Checking of Pointer Programs….Pages 397-412
PDL with Intersection and Converse Is Decidable….Pages 413-427
On Deciding Topological Classes of Deterministic Tree Languages….Pages 428-441
Complexity and Intensionality in a Type-1 Framework for Computable Analysis….Pages 442-461
Computing with Sequences, Weak Topologies and the Axiom of Choice….Pages 462-476
Light Functional Interpretation….Pages 477-492
Feasible Proofs of Matrix Properties with Csanky’s Algorithm….Pages 493-508
A Propositional Proof System for Log Space….Pages 509-524
Identifying Polynomial-Time Recursive Functions….Pages 525-540
Confluence of Shallow Right-Linear Rewrite Systems….Pages 541-556
The Ackermann Award 2005….Pages 557-565
Clemens Lautemann: 1951-2005 An Obituary ….Pages 566-566
Back Matter….Pages –