Computer Science Logic

Invited Lectures.- XML Navigation and Tarski’s Relation Algebras.- Verification in Predicate Logic with Time: Algorithmic Questions.- Note on Formal Analogical Reasoning in the Juridical Context.- An Abstract Strong Normalization Theorem.- Semantics and Logics.- On Bunched Polymorphism.- Distributed Control Flow with Classical Modal Logic.- A Logic of Coequations.- A Semantic Formulation of ???-Lifting and Logical Predicates for Computational Metalanguage.- Type Theory and Lambda Calculus.- Order Structures on Böhm-Like Models.- Higher-Order Matching and Games.- Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations.- On the Role of Type Decorations in the Calculus of Inductive Constructions.- Linear Logic and Ludics.- L-Nets, Strategies and Proof-Nets.- Permutative Logic.- Focusing the Inverse Method for Linear Logic.- Towards a Typed Geometry of Interaction.- Constraints.- From Pebble Games to Tractability: An Ambidextrous Consistency Algorithm for Quantified Constraint Satisfaction.- An Algebraic Approach for the Unsatisfiability of Nonlinear Constraints.- Finite Models, Decidability and Complexity.- Coprimality in Finite Models.- Towards a Characterization of Order-Invariant Queries over Tame Structures.- Decidability of Term Algebras Extending Partial Algebras.- Results on the Guarded Fragment with Equivalence or Transitive Relations.- The Modular Decomposition of Countable Graphs: Constructions in Monadic Second-Order Logic.- On the Complexity of Hybrid Logics with Binders.- The Complexity of Independence-Friendly Fixpoint Logic.- Closure Properties of Weak Systems of Bounded Arithmetic.- Verification and Model Checking.- Transfinite Extension of the Mu-Calculus.- Bounded Model Checking of Pointer Programs.- PDLwith Intersection and Converse Is Decidable.- On Deciding Topological Classes of Deterministic Tree Languages.- Constructive Reasoning and Computational Mathematics.- Complexity and Intensionality in a Type-1 Framework for Computable Analysis.- Computing with Sequences, Weak Topologies and the Axiom of Choice.- Light Functional Interpretation.- Feasible Proofs of Matrix Properties with Csanky’s Algorithm.- Implicit Computational Complexity and Rewriting.- A Propositional Proof System for Log Space.- Identifying Polynomial-Time Recursive Functions.- Confluence of Shallow Right-Linear Rewrite Systems.- Appendices.- The Ackermann Award 2005.- Clemens Lautemann: 1951-2005 An Obituary.

Includes supplementary material: sn.pub/extras