Accepted Papers

Murray Patterson, Yongmei Liu, Eugenia Ternovska, and Arvind Gupta
Grounding for Model Expansion in k-Guarded Formulas

Mikolaj Bojanczyk, Anca Muscholl, Thomas Schwentick, Luc Segoufin, and Claire David
Two-Variable Logic on Words with Data

Tomas Brazdil, Vaclav Brozek, Vojtech Forejt, and Antonin Kucera
Stochastic Games with Branching-Time Winning Objectives

Guillaume Burel, Claude Kirchner
An Abstract Completion Procedure for Cut Elimination in Deduction Modulo

Dexter Kozen
Coinductive Proof Principles for Stochastic Processes

Dietrich Kuske, Markus Lohrey
Monadic chain logic over iterations and applications to pushdown systems

Ugo Dal Lago
Context Semantics, Linear Logic and Computational Complexity

Marcelo Fiore, Sam Staton
A Congruence Rule Format for Name-Passing Process Calculi from Mathematical Structural Operational Semantics

Leona F. Fass
A Logical Look at Agents’ Problem-Solving on the Semantic Web

Jonathan Hayman, Glynn Winskel
Independence and Concurrent Separation Logic

Detlef Kaehler, Ralf Kuesters, and Thomas Wilke
A Dolev-Yao-based Definition of Abuse-free Protocols

Daniel Leivant
Matching explicit and modal reasoning about programs: a proof theoretic delineation of dynamic logic

Roberto Maieli, Paul Ruet
Interactive correctness criterion for multiplicative-additive proof-nets

Alexis Maciel, Toniann Pitassi
A Conditional Lower Bound for a System of Constant-Depth Proofs with Modular Connectives

Eldar Fischer, Frederic Magniez, and Michel de Rougemont
Approximate Satisfiability and Equivalence

Guoqiang Pan, Moshe Y. Vardi
Fixed-Parameter Hierarchies inside PSPACE

Filippo Bonchi, Ugo Montanari, and Barbara König
Saturated Semantics for Reactive Systems

Adam Barth, John C. Mitchell
Managing Digital Rights using Linear Logic

Daniele Varacca, Hagen Voelzer
Temporal logics and model checking for fairly correct systems

Julian Zinn, Rakesh Verma
A Polynomial-time Algorithm for Uniqueness of Normal Forms of Linear Shallow Term Rewrite Systems

Lutz Schröder, Dirk Pattinson
PSPACE bounds for rank-1 modal logics

Sharon Shoham, Orna Grumberg
3-Valued Abstraction: More Precision at Less Cost

Stephane Demri, Ranko Lazic
LTL with the Freeze Quantifier and Register Automata

Makoto Tatsuta, Mariangiola Dezani
Normalisation is insensible to lambda-term identity or difference

Benoit Larose, Cynthia Loten, and Claude Tardif
A Characterisation of First-Order Constraint Satisfaction Problems

Laura Chaubard, Jean-Eric Pin, and Howard Straubing
First order formulas with modular predicates

Luke Ong
On model-checking trees generated by higher-order recursion schemes

Soren Lassen
Head normal form bisimulation for pairs and the lambda-mu calculus

Nir Piterman, Amir Pnueli
Faster Solutions of Street and Rabin Games

Patricia Bouyer, Thomas Brihaye, and Fabrice Chevalier
Control in o-minimal hybrid systems

Aaron Hunter
Non-Closure Results for First-Order Spectra

Thomas Ball, Orna Kupferman
An Abstraction-Refinement Framework for Multi-Agent Systems

Orna Kupferman, Moshe Y. Vardi
Memoryful Branching-Time Logic

Matthew Parkinson, Richard Bornat, and Cristiano Calcagno
Variables as Resource in Hoare Logics

Anuj Dawar, Martin Grohe, Stephan Kreutzer, and Nicole Schweikardt
Approximation Schemes for First-Order Definable Optimization Problems

Thierry Coquand, Arnaud Spiwack
Proof of strong normalisation using domain theory

Olivier Laurent, Lorenzo Tortora de Falco
Obsessional cliques: a semantic characterization of bounded time complexity

Giulio Manzonetto, Antonino Salibra
Boolean algebras for lambda calculus

Nir Piterman
From Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata

Mikolaj Bojanczyk, Thomas Colcombet
Bounds in omega-regularity

Jørgen Villadsen
Nominalization in Intensional Type Theory

Emil Kiss, Matthew Valeriote
On tractability and congruence distributivity

Martin Otto
The boundedness problem for monadic universal first-order logic

Vineet Kahlon, Aarti Gupta
An Automata-theoretic Appraoch for Model Checking Threads for LTL Properties

Tachio Terauchi, Alex Aiken
On Typability for Rank-2 Intersection Types with Polymorphic Recursion

Catuscia Palamidessi, Vijay Saraswat, Frank D. Valencia, and Björn Victor
On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi-Calculus