Logic in Computer Science

(LICS)

The LICS Symposium aims to attract original papers of high quality on theoretical and practical topics in computer science that relate to logic in a broad sense, including algebraic, categorical and topological approaches. The symposium draws papers from a wide range of areas: abstract data types, automated deduction, categorical models, concurrency, constraint programming, constructive mathematics, database theory, domain theory, finite model theory, hybrid systems, logics of knowledge, lambda and combinatory calculi, linear logic, logical aspects of computational complexity, logics in artificial intelligence, logic programming, modal and temporal logics, model checking, program logic and semantics, rewriting, logical aspects of symbolic computing, software specification, type systems, and verification.

**Program Chair:** E. Clarke (CMU)

**Program Committee:** S. Buss (UC San Diego),
A. Emerson (UT Austin), S. German (IBM Watson), G. Gottlob (TU
Vienna), O. Grumberg (Technion), D. Howe (Bell Labs),
C. Kirchner (INRIA & CRIN), K. Kunen (Wisconsin), P. Lincoln
(SRI), J. Mitchell (Stanford), U. Montanari (Univ. Pisa),
P. Panangaden (McGill), F. Pfenning (CMU), J. Rushby (SRI),
C. Stirling (Edinburgh), A. Stolboushkin (UCLA), G. Winskel
(Aarhus).

**Conference Chair:** J.G. Riecke (Bell Labs).

**Publicity:** A. Felty (Bell Labs), D. Howe (Bell Labs).

**General Chair:** M.Y. Vardi (Rice University)

**Organizing Committee:** M. Abadi, S. Abramsky, S. Artemov,
E. Boerger, A. Borodin, W. Brauer, A. Bundy, S. Buss, E. Clarke,
R. Constable, A. Felty, U. Goltz, D. Howe, G. Huet,
J.-P. Jouannaud, D. Kapur, C. Kirchner, P. Kolaitis, D. Kozen,
T. Leighton, D. Leivant, A.R. Meyer, D. Miller, J. Mitchell,
Y. Moschovakis, M. Okada, P. Panangaden, J. Remmel, J. Riecke,
S. Ronchi della Rocca, A. Scedrov, D. Scott, J. Tiuryn,
M.Y. Vardi.

**Email:** *lics96@cs.cmu.edu*

**Finite Model Theory I: 9:15-10:30.** *Chair: K. Kunen.*

A Generalization of Fagin's Theorem

* J. Antonio Medina & Neil Immerman (University of Massachusetts)*

DATALOG SIRUPs Uniform Boundedness Is Undecidable

*
Jerzy Marcinkowski (University of Wroclaw)*

On the Structure of Queries in Constraint Query Languages

*
Michael Benedikt & Leonid Libkin (Bell Labs)*

**Coffee Break: 10:30-11:00.**

**Concurrency: 11:00-12:40.** *Chair: U. Montanari.*

A Fully Abstract Domain Model for the Pi-Calculus

*
Ian Stark
(University of Aarhus)*

A Fully-Abstract Model for the Pi-Calculus

*
M.P. Fiore
(University of Edinburgh),
E. Moggi
(Universita di Genova) &
D. Sangiorgi
(INRIA)*

Higher Dimensional Transition Systems

*
Gian Luca Cattani & Vladimiro Sassone
(University of Aarhus)*

An Algebraic Theory of Process Efficiency

*
V. Natarajan & Rance Cleaveland
(North Carolina State University)*

**Lunch Break: 12:40-14:15.**

**Types I: 14:15-15:30.** *Chair: J. Mitchell.*

The Subtyping Problem for Second-Order Types is Undecidable

*
Jerzy Tiuryn & Pawel Urzyczyn
(Warsaw University)*

Subtyping Dependent Types

*
David Aspinall
(University of Edinburgh) &
Adriana Compagnoni
(University of Cambridge)*

Reduction-Free Normalisation for a Polymorphic System

*
Thorsten Altenkirch
(University of Edinburgh),
Martin Hofmann & Thomas Streicher
(TH Darmstadt)*

**Coffee Break: 15:30-16:00.**

**Temporal Logic and Mu-Calculus: 16:00-17:40.** *Chair: E.A. Emerson.*

An Until Hierarchy for Temporal Logic

*
Kousha Etessami & Thomas Wilke
(DIMACS)*

Locally Linear Time Temporal Logic

*
R. Ramanujam
(Universität Kiel)*

A Modal Mu-Calculus for Durational Transition Systems

*
Helmut Seidl
(Universität Trier)*

Tarskian Set Constraints

*
David McAllester
(AT&T Laboratories),
Robert Givan
(MIT AI Laboratory),
Dexter Kozen
(Cornell University) &
Carl Witty
(MIT AI Laboratory)*

Design of a Proof Assistant

*
Gérard Huet
(INRIA Rocquencourt)*

**Coffee Break: 10:30-11:00.**

**Reasoning about Programs: 11:00-12:40.** *Chair: P. Lincoln.*

Reasoning about Local Variables with Operationally-Based Logical Relations

*
Andrew M. Pitts
(Cambridge University)*

The Essence of Parallel Algol

*
Stephen Brookes
(Carnegie Mellon University)*

Games and Full Abstraction for FPC

*
Guy McCusker
(Imperial College)*

A Temporal Logic Approach to Binding Time Analysis

*
Rowan Davies
(Carnegie Mellon University)*

**Lunch Break: 12:40-14:15.**

**Model Checking I: 14:15-15:30.** *Chair: S. German.*

Symbolic Protocol Verification with Queue BDDs

*
Patrice Godefroid & David E. Long
(Bell Labs)*

Reactive Modules

*
Rajeev Alur
(Bell Labs) &
Thomas A. Henzinger
(University of California at Berkeley)*

Model-checking of Correctness Conditions for Concurrent Objects

*
Rajeev Alur
(Bell Labs),
Ken McMillan
(Cadence Berkeley Labs) &
Doron Peled
(Bell Labs)*

**Coffee Break: 15:30-16:00.**

**Types II: 16:00-17:40.** *Chair: D. Howe.*

A Semantic View of Classical Proofs: Type-Theoretic, Categorical, and Denotational Characterizations

*
C.-H. L. Ong
(University of Oxford & National University of Singapore)*

Syntactic Considerations on Recursive Types

*
Martín Abadi
(Systems Research Center, Digital Equipment Corporation) &
Marcelo P. Fiore
(University of Edinburgh)*

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

*
Gerd G. Hillebrand
(University of Pennsylvania) &
Paris C. Kanellakis
(Brown University)*

A Linear Logical Framework

*
Iliano Cervesato & Frank Pfenning
(Carnegie Mellon University)*

**Business Meeting: 20:00-21:30.**

The Theory of Hybrid Automata

*Thomas A. Henzinger (University of California at Berkeley)*

*Abstract:* Hybrid automata, which combine discrete transition
graphs with continuous dynamical systems, are mathematical models
for digital systems that interact with analog environments.
Hybrid automata
can be viewed as infinite-state transition systems, and this view
gives insights into the structure of hybrid state spaces. For
example, for certain interesting classes of hybrid automata, language
equivalence, mutual similarity, or bisimilarity induce finite
quotients of infinite state spaces. These results can be exploited
by analysis techniques for finite-state systems.

**Coffee Break: 10:30-11:00.**

**Model Checking II: 11:00-12:40.** *Chair: O. Grumberg.*

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

*
Bernard Willems & Pierre Wolper
(Université de Liège)*

Efficient Model Checking via the Equational Mu-Calculus

*
Girish Bhat & Rance Cleaveland
(North Carolina State University)*

General Decidability Theorems for Infinite-State Systems

*
Parosh Aziz Abdulla
(Uppsala University),
Karlis Cerans
(University of Latvia),
Bengt Jonsson
(Uppsala University) &
Yih-Kuen Tsay
(National Taiwan University)*

Relating Word and Tree Automata

*
Orna Kupferman
(Bell Labs),
Shmuel Safra
(Tel Aviv University) &
Moshe Y. Vardi
(Rice University)*

**Lunch Break: 12:40-14:15.**

**Finite Model Theory II: 14:15-15:30.** *Chair: G. Gottlob.*

More about Recursive Structures: Descriptive Complexity and Zero-One Laws

*
Tirza Hirst & David Harel
(The Weizmann Institute of Science)*

On the Expressive Power of Variable-Confined Logics

*
Phokion G. Kolaitis
(University of California, Santa Cruz) &
Moshe Y. Vardi
(Rice University)*

Zero-One Laws for Gilbert Random Graphs

*
Gregory L. McColm
(University of South Florida)*

**Coffee Break: 15:30-16:00.**

**Semantics and Domains: 16:00-17:40.** *Chair: G. Winskel.*

When Scott is Weak on the Top

*
Abbas Edalat
(Imperial College)*

Integration in Real PCF

*
Abbas Edalat & Martín Hötzel Escardó
(Imperial College)*

Game Semantics and Abstract Machines

*
Vincent Danos
(Paris 7 & CNRS)
Hugo Herbelin
(Paris 7 & INRIA) &
Laurent Regnier
(LMD-CNRS Marseille)*

Semantics of Normal Logic Programs and Contested Information

*
Shekhar Pradhan
(University of Maryland, College Park & Central Missouri State University)*

**Joint Banquet with RTA: 19:00-22:00.** *Chair: C.A. Gunter.*

Dinner speech by Dana Scott on ``Some Reflections on Logic and Logicians''.

Lattices, Categories and Communication

*André Joyal (Université du Québec à Montréal)*

*Abstract:* We describe a theory of communication based on
free lattices and free bicomplete categories. It is based on a
game-theoretic representation of bicomplete categories. All our
results extend to enriched categories. In (*) we associate a two
player game to each term representing an element of a free
lattice. To a pair of terms we associate a three player game, a
mediator facing two opposites. A strategy for the mediator is
viewed as a communication strategy between the opposites. A
communication strategy is complete iff it is winning. The
mediator has a complete communication strategy iff the
corresponding terms can be compared in the free lattice. Here we
show that the objects and arrows of free bicomplete categories
have a similar game-theoretic interpretation. Two communication
strategies are operationally equivalent iff they define the same
arrow in the free bicomplete category. Many connectives of linear
logic have an interpretation in free bicomplete categories. Our
work suggests similarities between the world of computing and that
of financing.

*Reference: *
(*) "Free lattices, communication and money games".
In *Proceedings of the 10th International Congress of
Logic, Methodology and Philosophy of Science*. Firenze, August 1995.

**Coffee Break: 10:30-11:00.**

**Lambda Calculus: 11:00-12:40.** *Chair: F. Pfenning.*

Linear Logic, Monads and the Lambda Calculus

*
Nick Benton
(University of Cambridge) &
Philip Wadler
(University of Glasgow)*

On Order-Incompleteness and Finite Lambda Models

*
Peter Selinger
(University of Pennsylvania)*

Confluence and Preservation of Strong Normalisation in an Explicit Substitutions Calculus

*
César Muñoz
(INRIA)*

Completing Partial Combinatory Algebras with Unique Head-Normal Forms

*
Inge Bethke
(CWI & University of Utrecht),
Jan Willem Klop
(CWI & Vrije Universiteit) &
Roel de Vrijer
(Vrije Universiteit)*

**Lunch Break: 12:40-14:15.**

**Rewriting and Unification: 14:15-15:30.** *Chair: C. Kirchner.*

Complexity Analysis Based on Ordered Resolution

*
David Basin & Harald Ganzinger
(Max-Planck-Institut für Informatik)*

Solving Linear Equations over Semirings

*
Paliath Narendran
(State University of New York at Albany)*

Basic Paramodulation and Decidable Theories

*
Robert Nieuwenhuis
(Technical University of Catalonia)*

**Coffee Break: 15:30-16:00.**

**Complexity and Decidability: 16:00-17:40.** *Chair: A. Stolboushkin.*

Counting Modulo Quantifiers on Finite Linearly Ordered Trees

*
Juha Nurmonen
(University of Helsinki)*

Simultaneous Rigid E-Unification and Related Algorithmic Problems; Skolemization and Decidability Problems for Fragments of Intuitionistic Logic

*
Anatoli Degtyarev
(Uppsala University),
Yuri Matiyasevich
(Steklov Institute of Mathematics) &
Andrei Voronkov
(Uppsala University)*

On the Complexity of Abduction

*
Victor W. Marek
(University of Kentucky),
Anil Nerode
(Cornell University) &
Jeffrey B. Remmel
(University of California, San Diego)*

Decision Problems for Semi-Thue Systems with a Few Rules

*
Yuri Matiyasevich
(Steklov Institute of Mathematics) &
Géraud Sénizergues
(LaBRI, Université de Bordeaux)*

**FLoC Plenary Session: 20:00-21:30.** *Chair: M.Y. Vardi.*

Calculi for Interactions

*
R. Milner
(Cambridge University, United Kingdom)*