Message from the General Chair

Message from the Program Chair (PDF)

pp. x

Conference Organization (PDF)

pp. xi

Kleene Award for Best Student Paper - 1997 (PDF)

pp. xii

Reviewers (PDF)

pp. xiii

Rewriting & Deduction: Chair: Claude Kirchner

Combination of Compatible Reduction Orderings that are Total on Ground Terms (Abstract)

Franz Baader, RWTH Aachen

pp. 2

PDF

Automata-driven automated induction (Abstract)

A. Bouhoula, Comput. Sci. Lab., SRI Int., Menlo Park, CA, USA

J.-P. Jouannaud, Comput. Sci. Lab., SRI Int., Menlo Park, CA, USA

pp. 14

PDF

Ground Reducibility is EXPTIME-complete (Abstract)

Hubert Comon, CNRS and LSV, Ecole Normale Superieure de Cachan

Florent Jacquemard, MPI Saarbrucken

pp. 26

PDF

Strong Normalization of Explicit Substitutions via Cut Elimination in Proof Nets (Abstract)

Roberto Di Cosmo, LIENS-DMI LRI (CNRS URA 410)

Delia Kesner, LIENS-DMI LRI (CNRS URA 410)

pp. 35

PDF

Linear Logic & Game Semantics: Chair: Pat Lincoln

Temporal Linear Logic Specifications for Concurrent Processes (Abstract)

Max Kanovich, Russian State University for the Humanities

Takayasu Ito, Tohoku University

pp. 48

PDF

Full abstraction for functional languages with control (Abstract)

James Laird, University of Edinburgh

pp. 58

PDF

Believe it or not, AJM's games model is a model of classical linear logic (Abstract)

P. Baillot, CNRS, Marseille, France

V. Danos, CNRS, Marseille, France

T. Ehrhard, CNRS, Marseille, France

L. Regnier, CNRS, Marseille, France

pp. 68

PDF

Games and Definability for System F (Abstract)

Dominic James Doran Hughes, Oxford University Computing Laboratory

pp. 76

PDF

Model Checking: Chair: Ken McMillan

Boolean Expression Diagrams (Abstract)

Henrik Reif Andersen, Technical University of Denmark

Henrik Hulgaard, Technical University of Denmark

pp. 88

PDF

How much memory is needed to win infinite games? (Abstract)

S. Dziembowski, Inst. of Inf., Warsaw Univ., Poland

M. Jurdzinski, Inst. of Inf., Warsaw Univ., Poland

I. Walukiewicz, Inst. of Inf., Warsaw Univ., Poland

pp. 99

PDF

Quantitative Analysis and Model Checking (Abstract)

Michael Huth, Kansas State University

Marta Kwiatkowska, University of Birmingham

pp. 111

PDF

Concurrency: Chair: Matthew Hennessy

A Partially Deadlock-free Typed Process Calculus (Abstract)

Naoki Kobayashi, Department of Information Science, University of Tokyo

pp. 128

PDF

Unique Fixpoint Induction for Value-Passing Processes (Abstract)

Julian Rathke, University of Sussex

pp. 140

PDF

Bisimulation for Labelled Markov Processes (Abstract)

Richard Blute, University of Ottawa

Josee Desharnais, McGill University

Abbas Edalat, Imperial College of Science

Prakash Panangaden, Aarhus University

pp. 149

PDF

Temporal Logic & Automata: Chair: Colin Stirling

A Kleene theorem for timed automata (Abstract)

E. Asarin, Inst. for Inf. Transmission Problems, Moscow, Russia

P. Caspi, Inst. for Inf. Transmission Problems, Moscow, Russia

O. Maler, Inst. for Inf. Transmission Problems, Moscow, Russia

pp. 160

PDF

Automata, tableaus and a reduction theorem for fixpoint calculi in arbitrary complete lattices (Abstract)

David Janin, LaBRI, Universite' de Bordeaux I, France

pp. 172

PDF

An Exprssively Complete Linear Time Temporal Logic for Mazurkiewicz Traces. (Abstract)

P.S. Thiagarajan, SPIC Mathematical Institute

I. Walukiewicz, Institute of Informatics, Warsaw University

pp. 183

PDF

On the Complexity of Reasoning in Kleene Algebra (Abstract)

Dexter Kozen, Cornell University

pp. 195

PDF

Finite Model Theory: Chair: Anuj Dawar

On the Forms of Locality over Finite Models (Abstract)

Leonid Libkin, Bell Laboratories

pp. 204

PDF

Large finite structures with few L^k-types (Abstract)

Martin Grohe, Albert-Ludwigs-Universitaet Freiburg

pp. 216

PDF

First-Order Logic with Two Variables and Unary Temporal (Abstract)

Kousha Etessami, University of Aarhus

Moshe Y. Vardi, Rice University

Thomas Wilke, Institut fur Informatik und Prakt. Math Christian-Albrechts-Universitat zu Kiel

pp. 228

PDF

The Monadic Quantifier Alternation Hierarchy over Graphs is Infinite (Abstract)

Oliver Matz

Wolfgang Thomas

pp. 236

PDF

Semantics & Domain Theory I: Chair: Stephen Brookes

Semantics of Exact Real Arithmetic (Abstract)

Peter Potts, Imperial College

Abbas Edalat, Imperial College

Martin Escardo, Imperial College

pp. 248

PDF

A Relational Account of Call-by-Value Sequentially (Abstract)

Jon G. Riecke, Bell Laboratories

Anders Sandholm, Aarhus University

pp. 258

PDF

Complete Cuboidal Sets in Axiomatic Domain Theory (Abstract)

Marcelo Fiore, Laboratory for Foundations of Computer Science University of Edinburgh

Gordon Plotkin, Laboratory for Foundations of Computer Science University of Edinburgh

John Power, Laboratory for Foundations of Computer Science University of Edinburgh

pp. 268

PDF

Towards a Mathematical Operational Semantics (Abstract)

Daniele Turi, Laboratory for Foundations of Computer Science University of Edinburgh

Gordon Plotkin, Laboratory for Foundations of Computer Science University of Edinburgh

pp. 280

PDF

Decidability & Complexity Theory: Chair: Jan Krajicek

The "Hardest'' Natural Decidable Theory (Abstract)

Sergei Vorobyov, Max-Planck-Institut fuer Informatik

pp. 294

PDF

Two-variable logic with counting is decidable (Abstract)

Erich Graedel, RWTH Mathematische Grundlagen der Informatik

Martin Otto, RWTH Mathematische Grundlagen der Informatik

Eric Rosen, RWTH Mathematische Grundlagen der Informatik

pp. 306

PDF

Complexity of Two-Variable Logic with Counting (Abstract)

Leszek Pacholski, University of Wroclaw

Wieslaw Szwast, Institute of Mathematics University of Opole

Lidia Tendera, Institute of Mathematics University of Opole

pp. 318

PDF

Complexity of Power Default Reasoning (Abstract)

Guo-Qiang Zhang, University of Georgia

William C. Rounds, Artificial Intelligence Laboratory University of Michigan

pp. 328

PDF

Types and Constraints: Chair: Jens Palsberg

On the Cubic Bottleneck in Subtyping and Flow Analysis (Abstract)

Nevin Heintze, Bell Labs

David McAllester, AT&T Labs

pp. 342

PDF

The complexity of subtype entailment for simple types (Abstract)

F. Henglein, Dept. of Comput. Sci., Copenhagen Univ., Denmark

J. Rehof, Dept. of Comput. Sci., Copenhagen Univ., Denmark

pp. 352

PDF

Set constraints with intersection (Abstract)

W. Charatonik, Max-Planck-Inst. fur Inf., Saarbrucken, Germany

A. Podelski, Max-Planck-Inst. fur Inf., Saarbrucken, Germany

pp. 362

PDF

Tutorial: Chair: Claude Kirchner

Applications of Tree Automata in Rewriting and Lambda Calculus

Semantics & Domain Theory II: Chair: Pierre-Louis Curien

Induction and recursion on the partial real line via biquotients of bifree algebras (Abstract)

Martin Hotzel Escardo

pp. 376

PDF

Continuation models are universal for lambda-mu-calculus (Abstract)

Martin Hofmann, TH Darmstadt, FB

Thomas Streicher, TH Darmstadt, FB

pp. 387

PDF

Discrimination by Parallel Observers (Abstract)

Mariangiola Dezani-Ciancaglini, University of Torino

Jerzy Tiuryn, University of Warsaw

Pawel Urzyczyn:, University of Warsaw

pp. 396

PDF

Unification and Higher-Order Logic: Chair: Amy Felty

Ramified Higher-Order Unification (Abstract)

Jean Goubault-Larrecq, G.I.E. Dyade

pp. 410

PDF

Linear higher-order pre-unification (Abstract)

I. Cervesato, Dept. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA

F. Pfenning, Dept. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA

pp. 422

PDF

A Logic for Reasoning with Higher-Order Abstract Syntax (Abstract)

Raymond McDowell, University of Pennsylvania

Dale Miller, University of Pennsylvania

pp. 434

PDF

Author Index (PDF)

pp. 447