The Community for Technology Leaders
Logic in Computer Science, Symposium on (2004)
Turku, Finland
July 13, 2004 to July 17, 2004
ISSN: 1043-6871
ISBN: 0-7695-2192-4
TABLE OF CONTENTS

Preface (PDF)

pp. 0_9

Preface (PDF)

pp. ix

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

Model Checking Probabilistic Pushdown Automata (Abstract)

Richard Mayr , Albert-Ludwigs-University Freiburg, Germany
Anton? Kucera , Masaryk University, Czech Republic
Javier Esparza , University of Stuttgart, Germany
pp. 12-21

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

Michael Baldamus , Uppsala University, Sweden
Bj? Victor , Uppsala University, Sweden
Joachim Parrow , Uppsala University, Sweden
pp. 22-31

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
Session 2

Automatic Structures: Richness and Limitations (Abstract)

Bakhadyr Khoussainov , University of Auckland, New Zealand
Sasha Rubin , University of Auckland, New Zealand
Andre Nies , University of Auckland, New Zealand
Frank Stephan , National ICT Australia
pp. 44-53

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

James Worrell , Tulane University, New Orleans, LA
Jo? Ouaknine , Carnegie Mellon University, Pittsburgh, PA
pp. 54-63

Vector Addition Tree Automata (Abstract)

Bruno Guillaume , INRIA, France
Sylvain Salvati , INRIA, France
Philippe de Groote , INRIA, France
pp. 64-73
Session 3 (Short Presentations)
Session 4

Testing, Optimizaton, and Games (Abstract)

Mihalis Yannakakis , Columbia University, New York, NY
pp. 78-88
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

On the Automata Size for Presburger Arithmetic (Abstract)

Felix Klaedtke , Albert-Ludwigs-Universit?t Freiburg, Germany
pp. 110-119

From Automata to Formulas: Convex Integer Polyhedra (Abstract)

Louis Latour , Universit? de Li?ge, Belgium
pp. 120-129
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

A Sequent Calculus for Nominal Logic (Abstract)

James Cheney , Cornell University
Murdoch Gabbay , LIX ?cole Polytechnique
pp. 139-148
Session 8

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

S. Abramsky , Oxford University
C.-H. L. Ong , Oxford University
D. R. Ghica , Oxford University
I. D. B. Stark , Edinburgh University
A. S. Murawski , Oxford University
pp. 150-159

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

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

Patrice Godefroid , Bell Laboratories, Lucent Technologies
Luca de Alfaro , University of California, Santa Cruz
Radha Jagadeesan , School of CTI, DePaul University
pp. 170-179
Session 9

Proof Nets and Boolean Circuits (Abstract)

Kazushige Terui , National Institute of Informatics, Japan
pp. 182-191

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

Susumu Hayashi , Kobe University, Japan
Ulrich Kohlenbach , Darmstadt University of Technology, Germany
Yohji Akama , Tohoku University, Sendai, Japan
Stefano Berardi , University of Turin, Italy
pp. 192-201

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

On the Geometry of Interaction for Classical Logic (Abstract)

David Pym , University of Bath, England, UK
Carsten F?hrmann , University of Bath, England, UK
pp. 211-220
Session 10

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

Benoit Larose , Concordia University, Canada
V?ctor Dalmau , University Pompeu Fabra, Spain
Andrei Krokhin , University of Warwick, UK
pp. 232-241

Parametric Limits (Abstract)

Uday S. Reddy , University of Birmingham
Brian Dunphy , University of Illinois
pp. 242-251
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
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

The Sensible Graph Theories of Lambda Calculus (Abstract)

Antonino Salibra , Universit? Ca'Foscari di Venezia, Italia
Antonio Bucciarelli , Universit? Paris 7, France
pp. 276-285

A Symmetric Modal Lambda Calculus for Distributed Computing (Abstract)

Frank Pfenning , Carnegie Mellon
Robert Harper , Carnegie Mellon
Tom Murphy VII , Carnegie Mellon
Karl Crary , Carnegie Mellon
pp. 286-295
Session 13

Bisimulation: From The Origins to Today (Abstract)

Davide Sangiorgi , University of Bologna, Italy
pp. 298-302

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

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

Mike Barnett , Microsoft Research
David A. Naumann , Stevens Institute of Technology
pp. 313-323
Session 14

A Computational Interpretation of Open Induction (Abstract)

Ulrich Berger , University of Wales Swansea, UK
pp. 326

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

Multi-Clock Timed Networks (Abstract)

Johann Deneux , Uppsala University
Pritha Mahata , Uppsala University
Parosh Aziz Abdulla , Uppsala University
pp. 345-354
Session 15

A Landscape with Games in the Background (Abstract)

Igor Walukiewicz , Universit? Bordeaux-1 and CNRS, France
pp. 356-366

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
Session 16

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

Stephen Cook , University of Toronto
Phuong Nguyen , University of Toronto
pp. 378-387

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

Martin Grohe , Humboldt-Universit?t zu Berlin, Germany
J? Flum , Albert-Ludwigs Universit?t Freiburg, Germany
pp. 388-397

A Second-Order Theory for NL (Abstract)

Antonina Kolokolova , University of Toronto
Stephen Cook , University of Toronto
pp. 398-407
Session 17

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

Samson Abramsky , Oxford University Computing Laboratory
pp. 410-414

A Categorical Semantics of Quantum Protocols (Abstract)

Samson Abramsky , Oxford University Computing Laboratory
Bob Coecke , Oxford University Computing Laboratory
pp. 415-425

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
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

Equicardinality on Linear Orders (Abstract)

Kerkko Luosto , University of Helsinki
pp. 458-465

Author Index (PDF)

pp. 467
106 ms
(Ver )