Computer Science Logic: 23rd International Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7-11, 2009, Proceedings (Lecture Notes in Computer Science, 5771)

Invited Talks.- Algebra for Tree Languages.- Forcing and Type Theory.- Functional Interpretations of Intuitionistic Linear Logic.- Fixed-Point Definability and Polynomial Time.- Special Invited Talk to Commemorate the Centenary of Stephen Cole Kleene.- Kleene's Amazing Second Recursion Theorem.- Contributed Papers.- Typed Applicative Structures and Normalization by Evaluation for System F ? .- Jumping Boxes.- Tree-Width for First Order Formulae.- Algorithmic Analysis of Array-Accessing Programs.- Decidable Relationships between Consistency Notions for Constraint Satisfaction Problems.- Cardinality Quantifiers in MLO over Trees.- From Coinductive Proofs to Exact Real Arithmetic.- On the Relation between Sized-Types Based Termination and Semantic Labelling.- Expanding the Realm of Systematic Proof Theory.- EXPTIME Tableaux for the Coalgebraic ?-Calculus.- On the Word Problem for -Categories, and the Properties of Two-Way Communication.- Intersection, Universally Quantified, and Reference Types.- Linear Game Automata: Decidable Hierarchy Problems for Stripped-Down Alternating Tree Automata.- Enriching an Effect Calculus with Linear Types.- Degrees of Undecidability in Term Rewriting.- Upper Bounds on Stream I/O Using Semantic Interpretations.- Craig Interpolation for Linear Temporal Languages.- On Model Checking Boolean BI.- Efficient Type-Checking for Amortised Heap-Space Analysis.- Deciding the Inductive Validity of ????* Queries.- On the Parameterised Intractability of Monadic Second-Order Logic.- Automatic Structures of Bounded Degree Revisited.- Nondeterminism and Observable Sequentiality.- A Decidable Spatial Logic with Cone-Shaped Cardinal Directions.- Focalisation and Classical Realisability.- Decidable Extensions of Church's Problem.- Nested Hoare Triples and Frame Rules for Higher-Order Store.- A Complete Characterization of Observational Equivalence in Polymorphic ?-Calculus with General References.- Non-Commutative First-Order Sequent Calculus.- Model Checking FO(R) over One-Counter Processes and beyond.- Confluence of Pure Differential Nets with Promotion.- Decision Problems for Nash Equilibria in Stochastic Games.- On the Complexity of Branching-Time Logics.- Nominal Domain Theory for Concurrency.- The Ackermann Award 2009.