CSDL - Proceedings L

Message from the Program Chair (PDF)

pp. xi

Conference Organization (PDF)

pp. xii

Kleene Award for Best Student Papers (PDF)

pp. xiii

List of Reviewers (PDF)

pp. xiv

Finite Model Theory I: Chair: K. Kunen

A generalization of Fagin's theorem (Abstract)

J.A. Medina, Dept. of Comput. Sci., Massachusetts Univ., Amherst, MA, USA

N. Immerman, Dept. of Comput. Sci., Massachusetts Univ., Amherst, MA, USA

pp. 2

PDF

DATALOG SIRUPs uniform boundedness is undecidable (Abstract)

J. Marcinkowski, Theor. of Comput. Sci. Group, Wroclaw Univ., Poland

pp. 13

PDF

On the Structure of Queries in Constraint Query Languages (Abstract)

Michael Benedikt, Bell Labs

Leonid Libkin, Bell Labs

pp. 25

PDF

Concurrency: Chair: U. Montanari

A Fully Abstract Domain Model for the p-Calculus (Abstract)

Ian Stark, University of Aarhus, Denmark

pp. 36

PDF

A Fully-Abstract Model for the p-calculus (Abstract)

pp. 43

PDF

Higher Dimensional Transition Systems (Abstract)

Gian Luca Cattani, Aarhus University, Denmark

Vladimiro Sassone, Universita di Pisa, Italia

pp. 55

PDF

An Algebraic Theory of Process Efficiency (Abstract)

V. Natarajan, North Carolina State University

Rance Cleaveland, North Carolina State University

pp. 63

PDF

Types I: Chair: J. Mitchell

The Subtyping Problem for Second-Order Types is Undecidable (Abstract)

Jerzy Tiuryn, Warsaw University

Pawel Urzyczyn, Warsaw University

pp. 74

PDF

Subtyping Dependent Types (Abstract)

David Aspinall, University of Edinburgh

Adriana Compagnoni, University of Cambridge

pp. 86

PDF

Reduction-free normalisation for a polymorphic system (Abstract)

pp. 98

PDF

Temporal Logic and Calculus: Chair: E.A. Emerson

An Until Hierarchy for Temporal Logic (Abstract)

Kousha Etessami, Rutgers University

Thomas Wilke, Rutgers University

pp. 108

PDF

Locally linear time temporal logic (Abstract)

R. Ramanujam, Institute of Mathematical Sciences C. I. T. Campus, India

pp. 118

PDF

A Modal Mu-Calculus for Durational Transition Systems (Abstract)

Helmut Seidl, Fachbereich IV / Abt. Informatik Universitat Trier, Germany

pp. 128

PDF

Tarskian Set Constraints (Abstract)

pp. 138

PDF

Reasoning about Programs: Chair: P. Lincoln

Reasoning about local variables with operationally-based logical relations (Abstract)

A.M. Pitts, Comput. Lab., Cambridge Univ., UK

pp. 152

PDF

The essence of parallel Algol (Abstract)

S. Brookes, Dept. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA

pp. 164

PDF

Games and Full Abstraction for FPC (Abstract)

Guy McCusker, Imperial College, London

pp. 174

PDF

A temporal-logic approach to binding-time analysis (Abstract)

R. Davies, Dept. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA

pp. 184

PDF

Model Checking I: Chair: S. German

Symbolic Protocol Verification with Queue BDDs (Abstract)

Patrice Godefroid, Lucent Technologies

David E. Long, Lucent Technologies

pp. 198

PDF

Reactive Modules (Abstract)

Rajeev Alur

Thomas A. Henzinger

pp. 207

PDF

Model-checking of correctness conditions for concurrent objects (Abstract)

pp. 219

PDF

Types II: Chair: D. Howe

A semantic view of classical proofs: type-theoretic, categorical, and denotational characterizations (Abstract)

C.-H. L. Ong, University of Oxford and National University of Singapore

pp. 230

PDF

Syntactic Considerations on Recursive Types (Abstract)

Martin Abadi

Marcelo P. Fiore

pp. 242

PDF

On the Expressive Power of Simply Typed and Let-Polymorphic Lambda Calculi (Abstract)

Gerd Hillebrand, Fakultaet fuer Informatik, Germany

Paris Kanellakis, Brown University

pp. 253

PDF

A Linear Logical Framework (Abstract)

Iliano Cervesato

Frank Pfenning

pp. 264

PDF

Tutorial: Chair: J. Rushby

The theory of hybrid automata (Abstract)

T.A. Henzinger, Dept. of Electr. Eng. & Comput. Sci., California Univ., Berkeley, CA, USA

pp. 278

PDF

Model Checking II: Chair: O. Grumberg

Partial-Order Methods for Model Checking: From Linear Time to Branching Time (Abstract)

B. Willems & P. Wolper, Universite de Liege, BELGIUM

pp. 294

PDF

Efficient model checking via the equational /spl mu/-calculus (Abstract)

G. Bhat, Dept. of Comput. Sci., North Carolina State Univ., Raleigh, NC, USA

R. Cleaveland, Dept. of Comput. Sci., North Carolina State Univ., Raleigh, NC, USA

pp. 304

PDF

General decidability theorems for infinite-state systems (Abstract)

P.A. Abdulla, Dept. of Comput. Syst., Uppsala Univ., Sweden

K. Cerans, Dept. of Comput. Syst., Uppsala Univ., Sweden

B. Jonsson, Dept. of Comput. Syst., Uppsala Univ., Sweden

Yih-Kuen Tsay, Dept. of Comput. Syst., Uppsala Univ., Sweden

pp. 313

PDF

Relating word and tree automata (Abstract)

O. Kupferman, AT&T Bell Labs., Murray Hill, NJ, USA

S. Safra, AT&T Bell Labs., Murray Hill, NJ, USA

M.Y. Vardi, AT&T Bell Labs., Murray Hill, NJ, USA

pp. 322

PDF

Finite Model Theory II: Chair: G. Gottlob

More about recursive structures: descriptive complexity and zero-one laws (Abstract)

T. Hirst, Weizmann Inst. of Sci., Rehovot, Israel

D. Harel, Weizmann Inst. of Sci., Rehovot, Israel

pp. 334

PDF

On the expressive power of variable-confined logics (Abstract)

P.G. Kolaitis, Dept. of Comput. Sci., California Univ., Santa Cruz, CA, USA

M.Y. Vardi, Dept. of Comput. Sci., California Univ., Santa Cruz, CA, USA

pp. 348

PDF

Zero-one laws for Gilbert random graphs (Abstract)

G.L. McColm, Dept. of Math., Univ. of South Florida, Tampa, FL, USA

pp. 360

PDF

Semantics and Domains: Chair: G. Winskel

The Scott Topology Induces the Weak Topology (Abstract)

Abbas Edalat

pp. 372

PDF

Real PCF extended with integration (Abstract)

Martin Hotzel Escardo

Abbas Edalat

pp. 382

PDF

Game semantics and abstract machines (Abstract)

V. Danos, Paris VII Univ., France

H. Herbelin, Paris VII Univ., France

L. Regnier, Paris VII Univ., France

pp. 394

PDF

Semantics of Normal Logic Programs and Contested Information (Abstract)

Shekhar Pradhan, University of Maryland and Missouri State University

pp. 406

PDF

Lambda Calculus: Chair: F. Pfenning

Linear Logic, Monads and the Lambda Calculus (Abstract)

Nick Benton, University of Cambridge

Philip Wadler, University of Glasgow

pp. 420

PDF

Order-Incompleteness and Finite Lambda Models, Extended Abstract (Abstract)

Peter Selinger, University of Pennsylvania

pp. 432

PDF

Confluence and Preservation of Strong Normalisation in an Explicit Substitutions Calculus (Abstract)

Cesar A. Munoz, INRIA, Paris

pp. 440

PDF

Completing Partial Combinatory Algebras with Unique Head-Normal Forms (Abstract)

pp. 448

PDF

Rewriting and Unification;: Chair: C. Kirchner

Complexity Analysis Based on Ordered Resolution (Abstract)

David Basin, Max-Planck-Institut fuer Informatik, Germany

Harald Ganzinger, Max-Planck-Institut fuer Informatik, Germany

pp. 456

PDF

Solving linear equations over polynomial semirings (Abstract)

P. Narendran, Dept. of Comput. Sci., State Univ. of New York, Albany, NY, USA

pp. 466

PDF

Basic Paramodulation and Decidable Theories (Abstract)

Robert Nieuwenhuis, Technical University of Catalonia, Spain

pp. 473

PDF

Complexity and Decidability: Chair: A. Stolboushkin

Counting Modulo Quantifiers on Finite Linearly Ordered Trees (Abstract)

Juha Nurmonen, University of Helsinki

pp. 484

PDF

Simultaneous Rigid E-Unification and Related Algorithmic Problems (Abstract)

pp. 494

PDF

Decidability Problems for the Prenex Fragment of Intuitionistic Logic (Abstract)

Anatoli Degtyarev

Andrei Voronkov

pp. 503

PDF

On the Complexity of Abduction (Abstract)

Victor W. Marek, University of Kentucky

Anil Nerode, Cornell University

Jeffrey B. Remmel, University of California at La Jolla

pp. 513

PDF

Decision Problems for Semi-Thue Systems with a Few Rules (Abstract)

Yuri Matiyasevich, Steklov Institute of Mathematics of Russian Academy of Sciences

Geraud Senizergues, Universite de Bordeaux, France

pp. 523

PDF

FLoC Plenary Session: Chair: M.Y. Vardi

Index of Authors (PDF)

pp. 535