Message from the General Chair

Message from the Program Chair (PDF)

pp. x

Committees (PDF)

pp. xi

Additional Reviewers (PDF)

pp. xii

Kleene Award for Best Student Paper (PDF)

pp. xiii

Invited Speaker I

A Complete Proof Systems for QPTL (Abstract)

Yonit Kesten, Department of Computer Science Weizmann Institute of Science, Israel

Amir Pnueli, Department of Computer Science Weizmann Institute of Science, Israel

pp. 2

PDF

Session 1: Program Logics I: Chair: D. Kozen

Completeness of Kozen's Axiomatisation of the Propositional Mu-Calculus (Abstract)

Igor Walukiewicz, BRICS, Department of Computer Science University of Aarhus

pp. 14

PDF

Once and For All (Abstract)

Orna Kupferman, Department of Computer Science The Technion, Israel

Amir Pnueli, Department of Computer Science Weizmann Institute of Science, Israel

pp. 25

PDF

Complete Proof Systems for First Order Interval Temporal Logic (Abstract)

Bruno Dutertre, Department of Computer Science, Royal Holloway, University of London, United Kingdom

pp. 36

PDF

Session 2: Finite Models I I: Chair: V. Tannen

The Infinitary Logic of Sparse Random Graphs (Abstract)

James F. Lynch, Clarkson University

Jerzy Tyszkiewicz, Mathematische Grundlagen der Informatik, Aachen, Germany

pp. 46

PDF

Generalized Quantifiers and 0-1 Laws (Abstract)

Anuj Dawar, Department of Computer Science University of Wales, Swansea, U.K.

Erich Grädel, Mathematische Grundlagen der Informatik, Aachen, Germany

pp. 54

PDF

Relativized Logspace and Generalized Quantifiers Over Finite Structures (Abstract)

Georg Gottlob, Institut fuer Informationssysteme Technische Universitaet Wien, Wien, Austria

pp. 65

PDF

First-Order Queries on Finite Structures Over the Reals (Abstract)

Jan Paredaens, University of Antwerp (UIA)

Jan Van den Bussche, INRIA Rocquencourt, France

Dirk Van Gucht, Indiana University

pp. 79

PDF

Session 3: Model Checking and Verification: Chair: P. Sistla

Model-Checking of causality properties (Abstract)

pp. 90

PDF

On the complexity of modular model checking (Abstract)

M.Y. Vardi, Dept. of Comput. Sci., Rice Univ., Houston, TX, USA

pp. 101

PDF

Timing behavior analysis for real-time systems (Abstract)

Farn Wang

pp. 112

PDF

On the Verification Problem of Nonregular Properties for Nonregular Processes (Abstract)

pp. 123

PDF

Invited Speaker II

The Semantic Challenge of Verilog HDL (Abstract)

Mike Gordon, University of Cambridge, U.K.

pp. 136

PDF

Session 4: Theorem. Proving and AI:Chair: T. Henzinger

Uniform proofs and disjunctive logic programming (Abstract)

G. Nadathur, Dept. of Comput. Sci., Chicago Univ., IL, USA

D.W. Loveland, Dept. of Comput. Sci., Chicago Univ., IL, USA

pp. 148

PDF

Structural Cut Elimination (Abstract)

Frank Pfenning, Department of Computer Science Carnegie Mellon University, Pennsylvania

pp. 156

PDF

Paramodulation without Duplication (Abstract)

Christopher Lynch, INRIA Lorraine et CRIN Campus Scientifique, Cedex France

pp. 167

PDF

Complexity of Normal Default Logic and Related Modes of Nonmonotonic Reasoning (Abstract)

V. W. Marek, Computer Science Department, University of Kentucky, Lexington, KY

A. Nerode, Mathematical Sciences Institute Cornell University, New York

J.B. Remmel, Mathematics Department, University of California, La Jolla, California

pp. 178

PDF

Session 5: Concurrency I: Chair: C. Brown

Control Structures (Abstract)

Alex Mifsud, Dept of Computer Science, University of Malta, Msida, Malta

Robin Milner, Computer Laboratory, University of Cambridge UK

John Power, Computer Science Dept, University of Edinburgh, UK

pp. 188

PDF

Configuration Structures (Abstract)

R.J. Van Glabbeek, Computer Science Department,Stanford University, Stanford, CA, USA

G.D. Plotkin, Department of Computer Science, University of Edinburgh, UK

pp. 199

PDF

A Typed Calculus of Synchronous Processes (Abstract)

Simon Gay, Imperial College of Science Technology and Medicine

Rajagopal Nagarajan, Imperial College of Science Technology and Medicine

pp. 210

PDF

Modal ?-Types for Processes (Abstract)

Marino Miculan, Dipartimento di Matematica ed Informatica, Universita di Udine, Via delle Scienze, Italy

Fabio Gadducci, Dipartimento di Informatica -- Universita di Pisa Corso Italia, Italy

pp. 221

PDF

Session 6: Semantics I: Chair: M. Abadi

Games and Full Abstraction for the Lazy Lambda-Calculus (Abstract)

Samson Abramsky, Imperial College of Science, Technology and Medicine, London, United Kingdom

Guy McCusker, Imperial College of Science, Technology and Medicine, London, United Kingdom

pp. 234

PDF

Domain Theory in Stochastic Processes (Abstract)

Abbas Edalat, Department of Computing, Imperial College, London

pp. 244

PDF

A Fully Abstract Semantics for a Concurrent Functional Language with Monadic Types (Abstract)

Alan Jeffrey, School of Cognitive and Computing Sciences,Sussex Univ., UK

pp. 255

PDF

Intited Speaker III

Experience using type theory as a foundation for computer science (Abstract)

R.L. Constable, Cornell Univ., Ithaca, NY, USA

pp. 266

PDF

Session 7: Lambda Calculus amd Types: Chair: J. Tiuryn

Equality Between Functionals in the Presence of Coproducts (Abstract)

Daniel J. Dougherty, Department of Mathematics Wesleyan University USA

Ramesh Subrahmanyam, Department of Mathematics Wesleyan University USA

pp. 282

PDF

A logic of subtyping (Abstract)

G. Loop, CNRS, Ecole Normale Superieure, Paris, France

K. Milsted, CNRS, Ecole Normale Superieure, Paris, France

S. Soloviev, CNRS, Ecole Normale Superieure, Paris, France

pp. 292

PDF

Normalization and Extensionality (Abstract)

Adolfo Piperno, Universita di Roma "La Sapienza"

pp. 300

PDF

New Notions of Reduction and Non-Semantic Proofs of Strong Beta- Normalization in Typed Lambda Calculi (Abstract)

A.J. Kfoury, Boston University Department of Computer Science Boston, MA

J.B. Wells, Boston University Department of Computer Science Boston, MA

pp. 311

PDF

Session 8: Finite Models II: Chair: P. Kolaitis

Finitely Monotone Properties (Abstract)

Alexei P. Stolboushkin, Department of Mathematics University of California, Los Angeles

pp. 324

PDF

Tree Canonization and Transtive Closure (Abstract)

Kousha Etessami, Department of Computer Science University of Massachusetts at Amherst

Neil Immerman, Department of Computer Science University of Massachusetts at Amherst

pp. 331

PDF

Ptime Canonization for Two Variables with Counting (Abstract)

Martin Otto, Mathematische Grundlagen der Informatik, Germany

pp. 342

PDF

When do Fixed Point Logics Capture Complexity Classes? (Abstract)

Anil Seth, The Institute of Mathematical Sciences C.I.T. Campus, Madras-600113, INDIA

pp. 353

PDF

Session 9: Unification and Rewriting: Chair: L. Bachmair

Higher-order Unification via Explicit Substitutions (Abstract)

Gilles Dowek, INRIA-Rocquencourt

Therese Hardin, INRIA-Rocquencourt

Claude Kirchner, INRIA-Rocquencourt

pp. 366

PDF

Orderings, AC-theories and Symbolic Constraint Solving (Abstract)

H. Comon, CNRS, Univ. Paris-Sud, France

R. Nieuwenhuis, Technical Univ. Catalonia, Barcelona, Spain

A. Rubio, Technical Univ. Catalonia, Barcelona, Spain

pp. 375

PDF

Session 10 Model Checking II: Chair: EA. Emerson

Efficient On-the-Fly Model Checking for CTL (Abstract)

Girish Bhat, Department of Computer Science, North Carolina State University, Raleigh, NC

Rance Cleaveland, Department of Computer Science, North Carolina State University, Raleigh, NC

Orna Grumberg, Department of Computer Science, The Technion, Haifa, ISRAEL

pp. 388

PDF

Partial Model Checking (Abstract)

Henrik Reif Andersen, Department of Computer Science, Technical University of Denmark

pp. 398

PDF

Hardware Verification, Boolean Logic Programming, Boolean Functional Programming (Abstract)

Enrico Tronci, Dip. Matematica Pura ed Applicata, Universita' di L'Aquila, Coppito, L'Aquila, Italy

pp. 408

PDF

Session 11: Concurrency II: Chair: U. Goltz

Compositionality via Cut-Elimination: Hennessy-Milner Logic for an Arbitrary GSOS (Abstract)

Alex K. Simpson, LFCS, Department of Computer Science University of Edinburgh,UK

pp. 420

PDF

Compositional Testing Preorders for Probabilistic Processes (Abstract)

Bengt Jonsson, Department of Computer Systems, Uppsala University, Sweden

Wang Yi, Department of Computer Systems, Uppsala University, Sweden

pp. 431

PDF

Session 12: Semantics II: Chair: L. Ong

The Stone Gamut: A Coordinatization of Mathematics (Abstract)

Vaughan R. Pratt

pp. 444

PDF

Logically Presented Domains (Abstract)

Erik Palmgren

Viggo Stoltenberg-Hansen

pp. 455

PDF

Games Semantics for Full Propositional Linear Logic (Abstract)

Francois Lamarche, Department of Computing, Imperial College of Science and Technology,London UK

pp. 464

PDF

Session 13: Linear Logic: Chair: D. Miller

Decision Problems For Second-Order Linear Logic (Abstract)

Patrick Lincoln, SRI International

Natarajan Shankar, SRI International

Andre Scedrov, University of Pennsylvania

pp. 476

PDF

The Complexity of Neutrals in Linear Logic (Abstract)

Max I. Kanovich, Tohoku University, Japan

pp. 486

PDF

Decidability of Linear Affine Logic (Abstract)

A.P. Kopylov, Department of Mathematics and Mechanics Moscow State University, Moscow, Russia

pp. 496

PDF

Invited Speaker IV

Origins and Metamorphoses of The Trinity: Logic, Nets, Automata (Abstract)

Boris Trakhtenbrot, Tel Aviv University, Ramat Aviv 69978, Israel

pp. 506

PDF

Sequentiality, Second-order Monadic Logic and Tree Automata (Abstract)

H. Comon, Univ. Paris,France

pp. 508

PDF

Author Index (PDF)

pp. 518