| Invited Papers |
| Topological Queries in Spatial Databases / V. Vianu |
| The Consistency Dimension, Compactness, and Query Learning / J.L. Balcázar |
| Descriptive and Parameterized Complexity / M. Grohe |
| Logical Specification of Operational Semantics / P.D. Mosses |
| Constraint-Based Analysis of Broadcast Protocols / G. Delzanno ; J. Esparza ; A. Podelski |
| Contributed Papers |
| Descriptive Complexity, I |
| Descriptive Complexity Theory for Constraint Databases / E. Grädel ; S. Kreutzer |
| Applicative Control and Computational Complexity / D. Leivant |
| Verification |
| Applying Rewriting Techniques to the Verification of Erlang Processes / T. Arts ; J. Giesl |
| Difference Decision Diagrams / J. Møller ; J. Lichtenberg ; H.R. Andersen ; H. Hulgaard |
| Analysis of Hybrid Systems: An Ounce of Realism Can Save an Infinity of States / M. Fränzle |
| Verifying Liveness by Augmented Abstraction / Y. Kesten ; A. Pnueli |
| Temporal Logic |
| Signed Interval Logic / T.M. Rasmussen |
| Quantitative Temporal Logic / Y. Hirshfeld ; A. Rabinovich |
| An Expressively Complete Temporal Logic without Past Tense Operators for Mazurkiewicz Traces / V. Diekert ; P. Gastin |
| Lambda Calculus, Linear Logic |
| Using Fields and Explicit Substitutions to Implement Objects and Functions in a de Bruijn Setting / E. Bonelli |
| Closed Reductions in the λ-Calculus / M. Fernández ; I. Mackie |
| Kripke Resource Models of a Dependently-Typed, Bunched λ-Calculus / S. Ishtiaq ; D.J. Pym |
| A Linear Logical View of Linear Type Isomorphisms / V. Balat ; R. Di Cosmo |
| Logic Programming, Modal Logic, Description Logic |
| Choice Logic Programs and Nash Equilibria in Strategic Games / M. De Vos ; D. Vermeir |
| Resolution Method for Modal Logic with Well-Founded Frames / S. Hagihara ; N. Yonezaki |
| A NExpTime-Complete Description Logic Strictly Contained in C2 / S. Tobies |
| A Road-Map on Complexity for Hybrid Logics / C. Areces ; P. Blackburn ; M. Marx |
| Descriptive Complexity, II |
| MonadicNLIN and Quantifier-Free Reductions / C. Lautemann ; B. Weinzinger |
| Directed Reachability: From Ajtai-Fagin to Ehrenfeucht-Fraïssé Games / J. Marcinkowski |
| Fixpoint Alternation and the Game Quantifier / J.C. Bradfield |
| Logic and Complexity |
| Lower Bounds for Space in Resolution / J. Torán |
| Program Schemes, Arrays, Lindstrom Quantifiers and Zero-One Laws / I.A. Stewart |
| Open Least Element Principle and Bounded Query Computation / L.D. Blekemishev |
| Lambda Calculus, Type Theory |
| A Universal Innocent Game Model for the Bohm Tree Lambda Theory / A.D. Ker ; H. Nickau ; C.-H.L. Ong |
| Anti-Symmetry of Higher-Order Subtyping / A. Compagnoni ; H. Goguen |
| Safe Proof Checking in Type Theory with Y / H. Geuvers ; E. Poll ; J. Zwanenburg |
| Monadic Presentations of Lambda Terms Using Generalized Inductive Types / T. Altenkirch ; B. Reus |
| Linear Logic, Mu Calculus, Concurrency |
| A P-Time Completeness Proof for Light Logics / L. Roversi |
| On Guarding Nested Fixpoints / H. Seidl ; A. Neumann |
| A Logical Viewpoint on Process-Algebraic Quotients / A. Kučera |
| A Truly Concurrent Semantics for a Simple Parallel Programming Language / M. Mislove |
| Specification, Data Refinement |
| Specification Refinement with System F / J.E. Hannay |
| Pre-logical Relations / F. Honsell ; D. Sannella |
| Data-Refinement for Call-By-Value Programming Languages / Y. Kinoshita ; J. Power |
| Tutorials |
| Term Rewriting / A. Middeldorp |
| Interactive Theorem Proving Using Type Theory / D.J. Howe |
| Author Index |
| Invited Papers |
| Topological Queries in Spatial Databases / V. Vianu |
| The Consistency Dimension, Compactness, and Query Learning / J.L. Balcázar |
| Descriptive and Parameterized Complexity / M. Grohe |
| Logical Specification of Operational Semantics / P.D. Mosses |
| Constraint-Based Analysis of Broadcast Protocols / G. Delzanno ; J. Esparza ; A. Podelski |
