Invited Paper -- Semantical Evaluations as Monadic Second-Order Compatible Structure Transformations -- Contributed Papers -- Verification for Java's Reentrant Multithreading Concept -- On the Integration of Observability and Reachability Concepts -- Proving Correctness of Timed Concurrent Constraint Programs -- Generalised Regular MSC Languages -- On Compositional Reasoning in the Spi-calculus -- On Specification Logics for Algebra-Coalgebra Structures: Reconciling Reachability and Observability -- A First-Order One-Pass CPS Transformation -- The Demonic Product of Probabilistic Relations -- Minimizing Transition Systems for Name Passing Calculi: A Co-algebraic Formulation -- Varieties of Effects -- A Characterization of Families of Graphs in Which Election Is Possible -- Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds* -- Efficient Type Matching -- Higher-Order Pushdown Trees Are Easy -- Conflict Detection and Resolution in Access Control Policy Specifications -- Logics Admitting Final Semantics -- Model Checking Fixed Point Logic with Chop -- On Model Checking Durational Kripke Structures -- Model-Checking Infinite Systems Generated by Ground Tree Rewriting -- Bounded MSC Communication -- The Informatic Derivative at a Compact Element -- Heterogeneous Development Graphs and Heterogeneous Borrowing -- Notions of Computation Determine Monads -- A Calculus of Circular Proofs and Its Categorical Semantics -- Verifying Temporal Properties Using Explicit Approximants: Completeness for Context-free Processes -- Note on the Tableau Technique for Commutative Transition Systems -- A Semantic Basis for Local Reasoning -- Linearity and Bisimulation.