Special Issue for the Conference on Computer Science Logic CSL 2009


Editor: Reinhard Kahle, Erich Grädel

CSL 2009, the 18th Annual Conference (and 23rd International Workshop) of the European Association for Computer Science Logic, was held in Coimbra, Portugal, in September 2009. This special issue contains extended versions of papers presented at the conference.

The six papers of this collection were invited by the guest editors, and cover a wide range of topics represented at the CSL conference, including co-algebraic methods in computer science, finite model theory, intuitionistic and linear logic, model checking, mu-calculus, proof complexity, parametrized complexity, and real number computation. We are grateful to the authors for their excellent submissions. All papers were refereed according to the usual high standards of LMCS.

We would like to express our gratitude to the Programme Committee and the external reviewers for their help in selecting an excellent programme for CSL 2009, and to the authors and participants for their contributions to the success of the conference. Finally, we would like to thank the editors of LMCS for their support to publish this special issue.

Reinhard Kahle and Erich Grädel
Guest Editors and CSL 2009 Programme Chairs

1. From coinductive proofs to exact real arithmetic: theory and applications

Berger, Ulrich.
Based on a new coinductive characterization of continuous functions we extract certified programs for exact real number computation from constructive proofs. The extracted programs construct and combine exact real number algorithms with respect to the binary signed digit representation of […]

2. Functional Interpretations of Intuitionistic Linear Logic

Ferreira, Gilda ; Oliva, Paulo.
We present three different functional interpretations of intuitionistic linear logic ILL and show how these correspond to well-known functional interpretations of intuitionistic logic IL via embeddings of IL into ILL. The main difference from previous work of the second author is that […]

3. EXPTIME Tableaux for the Coalgebraic mu-Calculus

Cirstea, Corina ; Kupke, Clemens ; Pattinson, Dirk.
The coalgebraic approach to modal logic provides a uniform framework that captures the semantics of a large class of structurally different modal logics, including e.g. graded and probabilistic modal logics and coalition logic. In this paper, we introduce the coalgebraic mu-calculus, an extension of […]

4. On the Parameterized Intractability of Monadic Second-Order Logic

Kreutzer, Stephan.
One of Courcelle's celebrated results states that if C is a class of graphs of bounded tree-width, then model-checking for monadic second order logic (MSO_2) is fixed-parameter tractable (fpt) on C by linear time parameterized algorithms, where the parameter is the tree-width plus the size of the […]

5. Tree-width for first order formulae

Adler, Isolde ; Weyer, Mark.
We introduce tree-width for first order formulae \phi, fotw(\phi). We show that computing fotw is fixed-parameter tractable with parameter fotw. Moreover, we show that on classes of formulae of bounded fotw, model checking is fixed parameter tractable, with parameter the length of the formula. This […]

6. Pebble Games, Proof Complexity, and Time-Space Trade-offs

Nordstrom, Jakob.
Pebble games were extensively studied in the 1970s and 1980s in a number of different contexts. The last decade has seen a revival of interest in pebble games coming from the field of proof complexity. Pebbling has proven to be a useful tool for studying resolution-based proof systems when comparing […]