Computer Science Logic

1. Front Matter

   PDF

2. Invited Talks

   1. Algebra for Tree Languages

      • Mikołaj Bojańczyk

      Pages 1-1

   2. Forcing and Type Theory

      • Thierry Coquand

      Pages 2-2

   3. Functional Interpretations of Intuitionistic Linear Logic

      • Gilda Ferreira, Paulo Oliva

      Pages 3-19

   4. Fixed-Point Definability and Polynomial Time

      • Martin Grohe

      Pages 20-23

3. Special Invited Talk to Commemorate the Centenary of Stephen Cole Kleene

   1. Kleene’s Amazing Second Recursion Theorem

      • Yiannis N. Moschovakis

      Pages 24-39

4. Contributed Papers

   1. Typed Applicative Structures and Normalization by Evaluation for System F^ω

      • Andreas Abel

      Pages 40-54

   2. Jumping Boxes

      • Beniamino Accattoli, Stefano Guerrini

      Pages 55-70

   3. Tree-Width for First Order Formulae

      • Isolde Adler, Mark Weyer

      Pages 71-85

   4. Algorithmic Analysis of Array-Accessing Programs

      • Rajeev Alur, Pavol Černý, Scott Weinstein

      Pages 86-101

   5. Decidable Relationships between Consistency Notions for Constraint Satisfaction Problems

      • Albert Atserias, Mark Weyer

      Pages 102-116

   6. Cardinality Quantifiers in MLO over Trees

      • Vince Bárány, Łukasz Kaiser, Alexander Rabinovich

      Pages 117-131

   7. From Coinductive Proofs to Exact Real Arithmetic

      • Ulrich Berger

      Pages 132-146

   8. On the Relation between Sized-Types Based Termination and Semantic Labelling

      • Frédéric Blanqui, Cody Roux

      Pages 147-162

   9. Expanding the Realm of Systematic Proof Theory

      • Agata Ciabattoni, Lutz Straßburger, Kazushige Terui

      Pages 163-178

   10. EXPTIME Tableaux for the Coalgebraic μ-Calculus

       • Corina Cîrstea, Clemens Kupke, Dirk Pattinson

       Pages 179-193

   11. On the Word Problem for \({\it \Sigma\Pi}\)-Categories, and the Properties of Two-Way Communication

       • Robin Cockett, Luigi Santocanale

       Pages 194-208

   12. Intersection, Universally Quantified, and Reference Types

       • Mariangiola Dezani-Ciancaglini, Paola Giannini, Simona Ronchi Della Rocca

       Pages 209-224

   13. Linear Game Automata: Decidable Hierarchy Problems for Stripped-Down Alternating Tree Automata

       • Jacques Duparc, Alessandro Facchini, Filip Murlak

       Pages 225-239

   14. Enriching an Effect Calculus with Linear Types

       • Jeff Egger, Rasmus Ejlers Møgelberg, Alex Simpson

       Pages 240-254

The annual conference of the European Association for Computer Science Logic (EACSL), CSL 2009, was held in Coimbra (Portugal), September 7–11, 2009. The conference series started as a programme of International Workshops on Computer Science Logic, and then at its sixth meeting became the Annual C- ference of the EACSL. This conference was the 23rd meeting and 18th EACSL conference; it was organized at the Department of Mathematics, Faculty of S- ence and Technology, University of Coimbra. In response to the call for papers, a total of 122 abstracts were submitted to CSL 2009of which 89 werefollowedby a full paper. The ProgrammeCommittee selected 34 papers for presentation at the conference and publication in these proceedings. The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. The awardrecipient for 2009 was Jakob Nordstr¨ om. Citation of the award, abstract of the thesis, and a biographical sketch of the recipient may be found at the end of the proceedings. The award was sponsored for the years 2007–2009 by Logitech S.A.

• algorithmic analysis
• computer
• computer science
• decidability
• forcing
• formal languages
• intuitionistic logic
• logic
• mu-calculus
• polynomial time
• rewriting
• tree languages
• type theory
• undecidability
• word problem

• Mathematische Grundlagen der Informatik, RWTH Aachen, Aachen, Germany

  Erich Grädel

• CENTRIA and Departamento de Matemática, Universidade Nova de Lisboa, Caparica, Portugal

  Reinhard Kahle

Policies and ethics