Table of Contents

• Algebra for Tree LanguagesMikolaj Bojanczyk. 1 [doi]
• Forcing and Type TheoryThierry Coquand. 2 [doi]
• Functional Interpretations of Intuitionistic Linear LogicGilda Ferreira, Paulo Oliva. 3-19 [doi]
• Fixed-Point Definability and Polynomial TimeMartin Grohe. 20-23 [doi]
• Kleene s Amazing Second Recursion TheoremYiannis N. Moschovakis. 24-39 [doi]
• Typed Applicative Structures and Normalization by Evaluation for System F:::::::omega:::::::Andreas Abel. 40-54 [doi]
• Jumping BoxesBeniamino Accattoli, Stefano Guerrini. 55-70 [doi]
• Tree-Width for First Order FormulaeIsolde Adler, Mark Weyer. 71-85 [doi]
• Algorithmic Analysis of Array-Accessing ProgramsRajeev Alur, Pavol Cerný, Scott Weinstein. 86-101 [doi]
• Decidable Relationships between Consistency Notions for Constraint Satisfaction ProblemsAlbert Atserias, Mark Weyer. 102-116 [doi]
• Cardinality Quantifiers in MLO over TreesVince Bárány, Lukasz Kaiser, Alexander Rabinovich. 117-131 [doi]
• From Coinductive Proofs to Exact Real ArithmeticUlrich Berger. 132-146 [doi]
• On the Relation between Sized-Types Based Termination and Semantic LabellingFrédéric Blanqui, Cody Roux. 147-162 [doi]
• Expanding the Realm of Systematic Proof TheoryAgata Ciabattoni, Lutz Straßburger, Kazushige Terui. 163-178 [doi]
• EXPTIME Tableaux for the Coalgebraic ::::µ::::-CalculusCorina Cîrstea, Clemens Kupke, Dirk Pattinson. 179-193 [doi]
• On the Word Problem for SP{Sigma Pi}-Categories, and the Properties of Two-Way CommunicationJ. Robin B. Cockett, Luigi Santocanale. 194-208 [doi]
• Intersection, Universally Quantified, and Reference TypesMariangiola Dezani-Ciancaglini, Paola Giannini, Simona Ronchi Della Rocca. 209-224 [doi]
• Linear Game Automata: Decidable Hierarchy Problems for Stripped-Down Alternating Tree AutomataJacques Duparc, Alessandro Facchini, Filip Murlak. 225-239 [doi]
• Enriching an Effect Calculus with Linear TypesJeff Egger, Rasmus Ejlers Møgelberg, Alex Simpson. 240-254 [doi]
• Degrees of Undecidability in Term RewritingJörg Endrullis, Herman Geuvers, Hans Zantema. 255-270 [doi]
• Upper Bounds on Stream I/O Using Semantic InterpretationsMarco Gaboardi, Romain Péchoux. 271-286 [doi]
• Craig Interpolation for Linear Temporal LanguagesAmélie Gheerbrant, Balder ten Cate. 287-301 [doi]
• On Model Checking Boolean BIHeng Guo, Hanpin Wang, Zhongyuan Xu, Yongzhi Cao. 302-316 [doi]
• Efficient Type-Checking for Amortised Heap-Space AnalysisMartin Hofmann, Dulma Rodriguez. 317-331 [doi]
• Deciding the Inductive Validity of FOR ALL THERE EXISTS :::*::: QueriesMatthias Horbach, Christoph Weidenbach. 332-347 [doi]
• On the Parameterised Intractability of Monadic Second-Order LogicStephan Kreutzer. 348-363 [doi]
• Automatic Structures of Bounded Degree RevisitedDietrich Kuske, Markus Lohrey. 364-378 [doi]
• Nondeterminism and Observable SequentialityJames Laird. 379-393 [doi]
• A Decidable Spatial Logic with Cone-Shaped Cardinal DirectionsAngelo Montanari, Gabriele Puppis, Pietro Sala. 394-408 [doi]
• Focalisation and Classical RealisabilityGuillaume Munch-Maccagnoni. 409-423 [doi]
• Decidable Extensions of Church s ProblemAlexander Rabinovich. 424-439 [doi]
• Nested Hoare Triples and Frame Rules for Higher-Order StoreJan Schwinghammer, Lars Birkedal, Bernhard Reus, Hongseok Yang. 440-454 [doi]
• A Complete Characterization of Observational Equivalence in Polymorphic ::::lambda::::-Calculus with General ReferencesEijiro Sumii. 455-469 [doi]
• Non-Commutative First-Order Sequent CalculusMakoto Tatsuta. 470-484 [doi]
• Model Checking FO(R) over One-Counter Processes and beyondAnthony Widjaja To. 485-499 [doi]
• Confluence of Pure Differential Nets with PromotionPaolo Tranquilli. 500-514 [doi]
• Decision Problems for Nash Equilibria in Stochastic GamesMichael Ummels, Dominik Wojtczak. 515-529 [doi]
• On the Complexity of Branching-Time LogicsVolker Weber. 530-545 [doi]
• Nominal Domain Theory for ConcurrencyDavid Turner, Glynn Winskel. 546-560 [doi]
• The Ackermann Award 2009Johann A. Makowsky, Alexander A. Razborov. 561-565 [doi]