| 2009 | Nested Hoare Triples and Frame Rules for Higher-Order Store. | Jan Schwinghammer, Lars Birkedal, Bernhard Reus, Hongseok Yang |
| 2009 | Decidable Extensions of Church's Problem. | Alexander Rabinovich |
| 2009 | Focalisation and Classical Realisability. | Guillaume Munch-Maccagnoni |
| 2009 | Kleene's Amazing Second Recursion Theorem. | Yiannis N. Moschovakis |
| 2009 | A Decidable Spatial Logic with Cone-Shaped Cardinal Directions. | Angelo Montanari, Gabriele Puppis, Pietro Sala |
| 2009 | The Ackermann Award 2009. | Johann A. Makowsky, Alexander A. Razborov |
| 2009 | Nondeterminism and Observable Sequentiality. | James Laird |
| 2009 | Automatic Structures of Bounded Degree Revisited. | Dietrich Kuske, Markus Lohrey |
| 2009 | On the Parameterised Intractability of Monadic Second-Order Logic. | Stephan Kreutzer |
| 2009 | Deciding the Inductive Validity of FOR ALL THERE EXISTS | Matthias Horbach, Christoph Weidenbach |
| 2009 | Efficient Type-Checking for Amortised Heap-Space Analysis. | Martin Hofmann, Dulma Rodriguez |
| 2009 | On Model Checking Boolean BI. | Heng Guo, Hanpin Wang, Zhongyuan Xu, Yongzhi Cao |
| 2009 | Fixed-Point Definability and Polynomial Time. | Martin Grohe |
| 2009 | Craig Interpolation for Linear Temporal Languages. | Amlie Gheerbrant, Balder ten Cate |
| 2009 | Upper Bounds on Stream I/O Using Semantic Interpretations. | Marco Gaboardi, Romain Pchoux |
| 2009 | Functional Interpretations of Intuitionistic Linear Logic. | Gilda Ferreira, Paulo Oliva |
| 2009 | Degrees of Undecidability in Term Rewriting. | Jrg Endrullis, Herman Geuvers, Hans Zantema |
| 2009 | Enriching an Effect Calculus with Linear Types. | Jeff Egger, Rasmus Ejlers Mgelberg, Alex Simpson |
| 2009 | Linear Game Automata: Decidable Hierarchy Problems for Stripped-Down Alternating Tree Automata. | Jacques Duparc, Alessandro Facchini, Filip Murlak |
| 2009 | Intersection, Universally Quantified, and Reference Types. | Mariangiola Dezani-Ciancaglini, Paola Giannini, Simona Ronchi Della Rocca |
| 2009 | Forcing and Type Theory. | Thierry Coquand |
| 2009 | On the Word Problem for SP{Sigma Pi}-Categories, and the Properties of Two-Way Communication. | J. Robin B. Cockett, Luigi Santocanale |
| 2009 | EXPTIME Tableaux for the Coalgebraic | Corina Crstea, Clemens Kupke, Dirk Pattinson |
| 2009 | Expanding the Realm of Systematic Proof Theory. | Agata Ciabattoni, Lutz Straburger, Kazushige Terui |
| 2009 | Algebra for Tree Languages. | Mikolaj Bojanczyk |