Preface

Conference Organization (PDF)

pp. x-x

Program Committee (PDF)

pp. xi-xi

Referees (PDF)

pp. xii-xiii

Session 1

Model Checking Synchronized Products of Infinite Transition Systems (Abstract)

Stefan W?hrle, RWTH Aachen, Germany

Wolfgang Thomas, RWTH Aachen, Germany

pp. 2-11

PDF

Model Checking Probabilistic Pushdown Automata (Abstract)

Javier Esparza, University of Stuttgart, Germany

Anton? Kucera, Masaryk University, Czech Republic

Richard Mayr, Albert-Ludwigs-University Freiburg, Germany

pp. 12-21

PDF

Spi Calculus Translated to π--Calculus Preserving May-Tests (Abstract)

Michael Baldamus, Uppsala University, Sweden

Joachim Parrow, Uppsala University, Sweden

Bj? Victor, Uppsala University, Sweden

pp. 22-31

PDF

Transition Invariants (Abstract)

Andreas Podelski, Max-Planck-Institut f?r Informatik, Saarbr?cken, Germany

Andrey Rybalchenko, Max-Planck-Institut f?r Informatik, Saarbr?cken, Germany

pp. 32-41

PDF

Session 2

Automatic Structures: Richness and Limitations (Abstract)

Bakhadyr Khoussainov, University of Auckland, New Zealand

Andre Nies, University of Auckland, New Zealand

Sasha Rubin, University of Auckland, New Zealand

Frank Stephan, National ICT Australia

pp. 44-53

PDF

On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap (Abstract)

Jo? Ouaknine, Carnegie Mellon University, Pittsburgh, PA

James Worrell, Tulane University, New Orleans, LA

pp. 54-63

PDF

Vector Addition Tree Automata (Abstract)

Philippe de Groote, INRIA, France

Bruno Guillaume, INRIA, France

Sylvain Salvati, INRIA, France

pp. 64-73

PDF

Session 3 (Short Presentations)

Categorical Models of First-Order Classical Sequent Proofs

Lazy Structure Preserving Translation of Boolean Expressions into CNF

On Definability of Function Classes by Relational Constraints and Corresponding Galois Connections

On Abiteboul-Vianu Theorem for Fixed-Point Logics with Generalized Quantifiers

Ludics on Graphs. Towards Concurrency

The Geometry of Linear Ramified Recurrence

Separation and the Lambdamu-Calculus

Epistemic Logics of Imperfect Information for Multi-agent Communication

Session 4

Testing, Optimizaton, and Games (Abstract)

Mihalis Yannakakis, Columbia University, New York, NY

pp. 78-88

PDF

Proving Termination Assertions in Dynamic Logics (Abstract)

Daniel Leivant, Indiana University

pp. 89-98

PDF

Session 5

Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds (Abstract)

Sanjit A. Seshia, Carnegie Mellon University, Pittsburgh, PA

Randal E. Bryant, Carnegie Mellon University, Pittsburgh, PA

pp. 100-109

PDF

On the Automata Size for Presburger Arithmetic (Abstract)

Felix Klaedtke, Albert-Ludwigs-Universit?t Freiburg, Germany

pp. 110-119

PDF

From Automata to Formulas: Convex Integer Polyhedra (Abstract)

Louis Latour, Universit? de Li?ge, Belgium

pp. 120-129

PDF

Session 7

Feasible Proofs and Computations: Partnership and Fusion (Abstract)

Alexander A. Razborov, Institute for Advanced Study, School of Mathematics, Princeton, NJ

pp. 134-138

PDF

A Sequent Calculus for Nominal Logic (Abstract)

Murdoch Gabbay, LIX ?cole Polytechnique

James Cheney, Cornell University

pp. 139-148

PDF

Session 8

Nominal Games and Full Abstraction for the Nu-Calculus (Abstract)

S. Abramsky, Oxford University

D. R. Ghica, Oxford University

A. S. Murawski, Oxford University

C.-H. L. Ong, Oxford University

I. D. B. Stark, Edinburgh University

pp. 150-159

PDF

Games with Secure Equilibria (Abstract)

Krishnendu Chatterjee, University of California, Berkeley

Thomas A. Henzinger, University of California, Berkeley; EPFL, Switzerland

Marcin Jurdzinski, University of California, Berkeley; University of Warwick, UK

pp. 160-169

PDF

Three-Valued Abstractions of Games: Uncertainty, but with Precision (Abstract)

Luca de Alfaro, University of California, Santa Cruz

Patrice Godefroid, Bell Laboratories, Lucent Technologies

Radha Jagadeesan, School of CTI, DePaul University

pp. 170-179

PDF

Session 9

Proof Nets and Boolean Circuits (Abstract)

Kazushige Terui, National Institute of Informatics, Japan

pp. 182-191

PDF

An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles (Abstract)

Yohji Akama, Tohoku University, Sendai, Japan

Stefano Berardi, University of Turin, Italy

Susumu Hayashi, Kobe University, Japan

Ulrich Kohlenbach, Darmstadt University of Technology, Germany

pp. 192-201

PDF

The Omega Rule is II_2^0-Hard in the λβ-Calculus (Abstract)

Benedetto Intrigila, Universit? degli Studi di L'Aquila, Italy

Richard Statman, Carnegie-Mellon University, Pittsburgh, PA

pp. 202-210

PDF

On the Geometry of Interaction for Classical Logic (Abstract)

Carsten F?hrmann, University of Bath, England, UK

David Pym, University of Bath, England, UK

pp. 211-220

PDF

Session 10

Beyond Image-Finiteness: Labelled Transition Systems as a Stone Space (Abstract)

Michael Huth, Imperial College London

pp. 222-231

PDF

First-Order Definable Retraction Problems for Posets and Reflexive Graphs (Abstract)

V?ctor Dalmau, University Pompeu Fabra, Spain

Andrei Krokhin, University of Warwick, UK

Benoit Larose, Concordia University, Canada

pp. 232-241

PDF

Parametric Limits (Abstract)

Brian Dunphy, University of Illinois

Uday S. Reddy, University of Birmingham

pp. 242-251

PDF

Session 11

Self-Adjusting Computation (PDF)

Robert Harper, Carnegie Mellon University, Pittsburgh, PA

pp. 254-255

The Strength of Replacement in Weak Arithmetic (Abstract)

Stephen Cook, University of Toronto

Neil Thapen, University of Toronto

pp. 256-264

PDF

Session 12

Light Types for Polynomial Time Computation in Lambda-Calculus (Abstract)

Patrick Baillot, Universit? Paris-Nord, France

Kazushige Terui, National Institute of Informatics, Tokyo, Japan

pp. 266-275

PDF

The Sensible Graph Theories of Lambda Calculus (Abstract)

Antonio Bucciarelli, Universit? Paris 7, France

Antonino Salibra, Universit? Ca'Foscari di Venezia, Italia

pp. 276-285

PDF

A Symmetric Modal Lambda Calculus for Distributed Computing (Abstract)

Tom Murphy VII, Carnegie Mellon

Karl Crary, Carnegie Mellon

Robert Harper, Carnegie Mellon

Frank Pfenning, Carnegie Mellon

pp. 286-295

PDF

Session 13

Bisimulation: From The Origins to Today (Abstract)

Davide Sangiorgi, University of Bologna, Italy

pp. 298-302

PDF

Congruence for SOS with Data (Abstract)

MohammadReza Mousavi, Eindhoven University of Technology (TU/e), The Netherlands

Michel Reniers, Eindhoven University of Technology (TU/e), The Netherlands

Jan Friso Groote, Eindhoven University of Technology (TU/e), The Netherlands

pp. 303-312

PDF

Towards Imperative Modules: Reasoning about Invariants and Sharing of Mutable State (Abstract)

David A. Naumann, Stevens Institute of Technology

Mike Barnett, Microsoft Research

pp. 313-323

PDF

Session 14

A Computational Interpretation of Open Induction (Abstract)

Ulrich Berger, University of Wales Swansea, UK

pp. 326

PDF

The Existence of Finite Abstractions for Branching Time Model Checking (Abstract)

Dennis Dams, Bell Labs, Lucent Technologies, Murray Hill, NJ

Kedar S. Namjoshi, Bell Labs, Lucent Technologies, Murray Hill, NJ

pp. 335-344

PDF

Multi-Clock Timed Networks (Abstract)

Parosh Aziz Abdulla, Uppsala University

Johann Deneux, Uppsala University

Pritha Mahata, Uppsala University

pp. 345-354

PDF

Session 15

A Landscape with Games in the Background (Abstract)

Igor Walukiewicz, Universit? Bordeaux-1 and CNRS, France

pp. 356-366

PDF

An Algebraic Approach to the Complexity of Propositional Circumscription (Abstract)

Gustav Nordh, Link?pings Universitet, Sweden

Peter Jonsson, Link?pings Universitet, Sweden

pp. 367-376

PDF

Session 16

VTC⁰: A Second-Order Theory for TC⁰ (Abstract)

Phuong Nguyen, University of Toronto

Stephen Cook, University of Toronto

pp. 378-387

PDF

Model-Checking Problems as a Basis for Parameterized Intractability (Abstract)

J? Flum, Albert-Ludwigs Universit?t Freiburg, Germany

Martin Grohe, Humboldt-Universit?t zu Berlin, Germany

pp. 388-397

PDF

A Second-Order Theory for NL (Abstract)

Stephen Cook, University of Toronto

Antonina Kolokolova, University of Toronto

pp. 398-407

PDF

Session 17

High-Level Methods for Quantum Computation and Information (Abstract)

Samson Abramsky, Oxford University Computing Laboratory

pp. 410-414

PDF

A Categorical Semantics of Quantum Protocols (Abstract)

Samson Abramsky, Oxford University Computing Laboratory

Bob Coecke, Oxford University Computing Laboratory

pp. 415-425

PDF

Semantics of a Sequential Language for Exact Real-Number Computation (Abstract)

J. Raymundo Marcial-Romero, University of Birmingham, England

Mart?n H. Escard?, University of Birmingham, England

pp. 426-435

PDF

Session 18

The Succinctness of First-Order Logic on Linear Orders (Abstract)

Martin Grohe, Humboldt-Universit?t Berlin, Germany

Nicole Schweikardt, Humboldt-Universit?t Berlin, Germany

pp. 438-447

PDF

A Graph of a Relational Structure and Constraint Satisfaction Problems (Abstract)

Andrei A. Bulatov, University of Oxford, UK

pp. 448-457

PDF

Equicardinality on Linear Orders (Abstract)

Kerkko Luosto, University of Helsinki

pp. 458-465

PDF

Author Index (PDF)

pp. 467-467