The Community for Technology Leaders
Logic in Computer Science, Symposium on (2006)
Seattle, Washington
Aug. 12, 2006 to Aug. 15, 2006
ISSN: 1043-6871
ISBN: 0-7695-2631-4
TABLE OF CONTENTS
Introduction

Reviewers (PDF)

pp. xii
Introduction

Foreward (PDF)

pp. ix
Introduction

Reviewers (PDF)

pp. xii
Plenary Talk
Session 1: Complexity and Decidability

Two-Variable Logic on Words with Data (Abstract)

Mikolaj Bojanczyk , Warsaw University
Thomas Schwentick , Dortmund University
Anca Muscholl , LIAFA, Paris VII
Claire David , LIAFA, Paris VII
Luc Segoufin , INRIA, Paris XI
pp. 7-16

LTL with the Freeze Quantifier and Register Automata (Abstract)

Stephane Demri , INRIA Futurs, France
Ranko Lazic , University of Warwick, UK
pp. 17-26

Fixed-Parameter Hierarchies inside PSPACE (Abstract)

Moshe Y. Vardi , Rice University, USA
Guoqiang Pan , Rice University, USA
pp. 27-36

The Boundedness Problem for Monadic Universal First-Order Logic (Abstract)

Martin Otto , Technische Universitat Darmstadt, Germany
pp. 37-48
Session 2: Concurrency

On the Expressiveness of Linearity vs Persistence in the Asychronous Pi-Calculus (Abstract)

Catuscia Palamidessi , INRIA, France
Frank D. Valencia , CNRS, France
Vijay Saraswat , IBM TJ Watson Research Lab, USA
Bjorn Victor , Uppsala University, Sweden
pp. 59-68

Saturated Semantics for Reactive Systems (Abstract)

Filippo Bonchi , University of Pisa
Ugo Montanari , University of Pisa
Barbara Konig , University of Duisburg-Essen
pp. 69-80
Session 3: Pushdown Systems

Monadic Chain Logic Over Iterations and Applications to Pushdown Systems (Abstract)

Markus Lohrey , Universitat Stuttgart, Germany
Dietrich Kuske , Universitat Leipzig, Germany
pp. 91-100

An Automata-Theoretic Approach for Model Checking Threads for LTL Propert (Abstract)

Vineet Kahlon , NEC Labs America, USA
Aarti Gupta , NEC Labs America, USA
pp. 101-110

On Typability for Rank-2 Intersection Types with Polymorphic Recursion (Abstract)

Tachio Terauchi , University of California, Berkeley, USA
Alex Aiken , Stanford University, USA
pp. 111-122
Invited Talk

Adapting Logics (PDF)

Andreas Blass , Microsoft Research, USA
pp. 123
Session 4: Logics of Program

Managing Digital Rights using Linear Logic (Abstract)

Adam Barth , Stanford University, USA
John C. Mitchell , Stanford University, USA
pp. 127-136

Variables as Resource in Hoare Logics (Abstract)

Richard Bornat , Middlesex University, UK
Matthew Parkinson , Middlesex University, UK
Cristiano Calcagno , University of London, UK
pp. 137-146

Independence and Concurrent Separation Logic (Abstract)

Glynn Winskel , University of Cambridge
Jonathan Hayman , University of Cambridge
pp. 147-156
Session 5: Proof Theory

Context Semantics, Linear Logic and Computational Complexity (Abstract)

Ugo Dal Lago , Universite Paris 13, France
pp. 169-178

Conditional Lower Bound for a System of Constant-Depth Proofs with Modular Connectives (Abstract)

Toniann Pitassi , University of Toronto, Canada
Alexis Maciel , Clarkson University, USA
pp. 189-200
Session 6: Model Theory

A Characterisation of First-Order Constraint Satisfaction Problems (Abstract)

Cynthia Loten , Royal Military College of Canada, Canada
Benoit Larose , Concordia University, Canada
Claude Tardif , Royal Military College of Canada, Canada
pp. 201-210

First Order Formulas with Modular Ppredicates (Abstract)

Howard Straubing , Boston College, USA
Laura Chaubard , Universit?e Paris VII, France
Jean-Eric Pin , Universit?e Paris VII, France
pp. 211-220

On Tractability and Congruence Distributivity (Abstract)

Matthew Valeriote , McMaster University, Canada
Emil Kiss , Eotvos University, Hungary
pp. 221-230

PSPACE Bounds for Rank-1 Modal Logics (Abstract)

Dirk Pattinson , University of Leicester
Lutz Schroder , Universitat Bremen
pp. 231-242
Invited Talk

Avoiding Determinization (Abstract)

Orna Kupferman , Hebrew University, Israel
pp. 243-254
Session 7: Temporal Logics and Automata

From Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata (Abstract)

Nir Piterman , Ecole Polytechnique F?ed?eral de Lausanne (EPFL)
pp. 255-264

Memoryful Branching-Time Logic (Abstract)

Orna Kupferman , Hebrew University, Israel
Moshe Y. Vardi , Rice University, USA
pp. 265-274

Faster Solutions of Rabin and Streett Games (Abstract)

Amir Pnueli , Weizmann Institute of Science, Israel
Nir Piterman , EPFL, Switzerland
pp. 275-284

Bounds in w-Regularity (Abstract)

Thomas Colcombet , CNRS/IRISA, France
Mikolaj Bojanczyk , LIAFA, France
pp. 285-296
Session 8: Lambda Calculus

A Proof of Strong Normalisation using Domain Theory (Abstract)

Thierry Coquand , Chalmers Tekniska Hijgskola, Sweden
Arnaud Spiwack , Ecole Norrnale SupCrieure de Cachan, France
pp. 307-316

Boolean Algebras for Lambda Calculus (Abstract)

A. Salibra , Universita Ca?Foscari di Venezia, Italy
G. Manzonetto , Universite Paris 7, France
pp. 317-326

Normalisation is Insensible to \lambda-Term Identity or Difference (Abstract)

Mariangiola Dezani-Ciancaglini , Dipartimento di Informatica, Italy
Makoto Tatsuta , National Institute of Informatics, Japan
pp. 327-338
Keynote Session: Celebrating Birth Centennial of Kurt Godel
Invited Talk
Session 9: Timed and Stochastic Systems

Coinductive Proof Principles for Stochastic Processes (Abstract)

Dexter Kozen , Cornell University, USA
pp. 359-366

Control in o-minimal Hybrid Systems (Abstract)

Fabrice Chevalier , LSV - CNRS & ENS de Cachan, France
Thomas Brihaye , Universite de Mons-Hainaut, Belguim
Patricia Bouyer , LSV - CNRS & ENS de Cachan, France
pp. 367-378
Session 10: Verification

An Abstraction-Refinement Framework for Multi-Agent Systems (Abstract)

Thomas Ball , Microsoft Research, USA
Orna Kupferman , Hebrew University, Israel
pp. 379-388

Temporal Logics and Model Checking for Fairly Correct Systems (Abstract)

Daniele Varacca , Imperial College London, UK
Hagen V?lzer , Universit?t zu L?beck, Germany
pp. 389-398

3-Valued Abstraction: More Precision at Less Cost (Abstract)

Orna Grumberg , Technion, Israel
Sharon Shoham , Technion, Israel
pp. 399-410
Session 11: Approximations

Approximation Schemes for First-Order Definable Optimisation Problems (Abstract)

Anuj Dawar , University of Cambridge, U.K.
Stephan Kreutzer , Humboldt-Universitat zu Berlin, Germany
Nicole Schweikardt , Humboldt-Universitat zu Berlin, Germany
Martin Grohe , Humboldt-Universitat zu Berlin, Germany
pp. 411-420

Approximate Satisfiability and Equivalence (Abstract)

Michel de Rougemont , Universite Paris II, France
Eldar Fischer , Technion, Israel
Frederic Magniez , Universite Paris-Sud, France
pp. 421-430
Author Index

Author Index (PDF)

pp. 431
105 ms
(Ver )