11th Annual IEEE Symposium on
Logic in Computer Science

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


Conference Program

Friday, 26 July 1996

Reception: 17:30-19:30.

Saturday, 27 July 1996

Welcome: 9:00-9:15.

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)

Sunday, 28 July 1996

Plenary Session with RTA: 9:15-10:30. Chair: E. Clarke.

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.

Monday, 29 July 1996

Tutorial: 9:15-10:30. Chair: J. Rushby.

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''.

Tuesday, 30 July 1996

Tutorial: 9:15-10:30. Chair: P. Panangaden.

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)

[Next] [Prev] [Contents] FLoC homepage