The Community for Technology Leaders
Logic in Computer Science, Symposium on (2001)
Boston, Massachusetts
June 16, 2001 to June 19, 2001
ISBN: 0-7695-1281-X
TABLE OF CONTENTS

A dichotomy in the complexity of propositional circumscription (PDF)

L.M. Kirousis , Dept. of Comput. Eng. & Inf., Patras Univ., Greece
pp. 71-80

Foreword (PDF)

pp. x
Invited Talk - Chair: Joseph Y. Halpern

Probabilistic Polynomial-Time Process Calculus and Security Protocol Analysis (Abstract)

J. Mitchell , Stanford University
A. Ramanathan , Stanford University
V. Teague , Stanford University
A. Scedrov , University of Pennsylvania
pp. 0003
Session 1 - Chair: Jean-Pierre Jouannaud

Light affine lambda calculus and polytime strong normalization (PDF)

K. Terui , Dept. of Philos., Keio Univ., Tokyo, Japan
pp. 209-220
Session 1 - Chair: Jean-Pierre Jouannaud

A Decision Procedure for an Extensional Theory of Arrays (Abstract)

Aaron Stump , Stanford University
Clark W. Barrett , Stanford University
David L. Dill , Stanford University
Jeremy Levitt , 0-In Design Automation, Inc.
pp. 0029

On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups (Abstract)

Guillem Godoy , Technical University of Catalonia
Robert Nieuwenhuis , Technical University of Catalonia
pp. 0038
Invited Talk - Chair: Jean-Pierre Jouannaud

Successive Approximation of Abstract Transition Relations (Abstract)

Satyaki Das , Stanford University
David L. Dill , Stanford University
pp. 0051
Session 2 - Chair: Pawel Urzyczyn

A Bound on Attacks on Payment Protocols (Abstract)

Scott D. Stoller , SUNY at Stony Brook
pp. 0061

From verification to control: dynamic programs for omega-regular objectives (PDF)

L. de Alfaro , Dept. of Electr. Eng. & Comput. Sci., California Univ., Berkeley, CA, USA
pp. 279-290
Session 3 - Chair: Radha Jaghadeesan

A Fully Abstract Game Semantics of Local Exceptions (Abstract)

J. Laird , University of Sussex
pp. 0105

A Universal Characterization of the Closed Euclidean Interval (Abstract)

Martín H. Escardó , University of Birmingham
Alex K. Simpson , University of Edinburgh
pp. 0115

Strong normalisation in the /spl pi/-calculus (PDF)

N. Yoshida , Dept. of Math. & Comput. Sci., Leicester Univ., UK
pp. 311-322
Session 4 - Chair: Michel de Rougemont

A continuum of theories of lambda calculus without semantics (Abstract)

A. Salibra , Dipt. di Inf., Venezia Univ., Italy
pp. 334-343
Session 4 - Chair: Michel de Rougemont

On Definability of Order in Logic with Choice (Abstract)

Taneli Huuskonen , University of Helsinki
Tapani Hyttinen , University of Helsinki
pp. 0167
Invited Talk - Chair: Erich Graedel
Session 5 - Chair: Erich Graedel

A Second-Order System for Polytime Reasoning Using Gr?del's Theorem (Abstract)

Stephen Cook , University of Toronto
Antonina Kolokolova , University of Toronto
pp. 0177

The Crane Beach Conjecture (Abstract)

David A. Mix Barrington , University of Massachusetts
Neil Immerman , University of Massachusetts
Clemens Lautemann , Johannes Gutenberg-Universit?t Mainz
Nicole Schweikardt , Johannes Gutenberg-Universit?t Mainz
Denis Thérien , McGill University
pp. 0187

An n! Lower Bound on Formula Size (Abstract)

Micah Adler , UMass, Amherst
Neil Immerman , UMass, Amherst
pp. 0197
Session 6 - Chair: Nevin Heintze

Dependent Types for Program Termination Verification (Abstract)

Hongwei Xi , University of Cincinnati
pp. 0231
Short Paper Session - Chair: Joseph Y. Halpern
Invited Talk - Chair: Ron van der Meyden

Foundational Proof-Carrying Code (Abstract)

Andrew W. Appel , Princeton University
pp. 0247
Session 7 - Chair: Parosh Abdulla

Intuitionistic Linear Logic and Partial Correctness (Abstract)

Dexter Kozen , Cornell University
Jerzy Tiuryn , Warsaw University
pp. 0259

Perturbed Turing Machines and Hybrid Systems (Abstract)

Eugene Asarin , VERIMAG
Ahmed Bouajjani , LIAFA, University of Paris 7
pp. 0269

Deterministic Generators and Games for Ltl Fragments (Abstract)

Rajeev Alur , University of Pennsylvania
Salvatore La Torre , University of Pennsylvania
pp. 0291
Session 8 - Chair: Adolfo Piperno
Session 9 - Chair: Hubert Comon

Focus Games for Satisfiability and Completeness of Temporal Logic (Abstract)

Martin Lange , University of Edinburgh
Colin Stirling , University of Edinburgh
pp. 0357

Safety and Liveness in Branching Time (Abstract)

Panagiotis Manolios , University of Texas, Austin
Richard Trefler , AT&T Labs-Research
pp. 0366
Short Papers
Invited Talk - Chair: Michel de Rougemont
Session 10 - Chair: Rance Cleaveland

Synthesizing Distributed Systems (Abstract)

Orna Kupferman , Hebrew University
Moshe Y. Vardi , Rice University
pp. 0389

Permutation Rewriting and Algorithmic Verification (Abstract)

Ahmed Bouajjani , LIAFA, Universit? Paris VII
Anca Muscholl , LIAFA, Universit? Paris VII
Tayssir Touili , LIAFA, Universit? Paris VII
pp. 0399

Temporal Logic Query Checking (Abstract)

Glenn Bruns , Bell Laboratories, Lucent Technologies
Patrice Godefroid , Bell Laboratories, Lucent Technologies
pp. 0409
Session 11 - Chair: Ron van der Meyden

Typechecking XML Views of Relational Databases (Abstract)

Noga Alon , Tel Aviv University
Tova Milo , Tel Aviv University
Frank Neven , Limburgs Universitair Centrum
Dan Suciu , University of Washington
Victor Vianu , U.C. San Diego
pp. 0421

Author Index (PDF)

pp. 0441
105 ms
(Ver 3.3 (11022016))