SUNDAY , JUNE 25
6:00 - 8:00 Welcome Reception
MONDAY , JUNE 26
8:50 - 9:00 Introduction
John Mitchell, LICS General Chair
9:00 - 10:00 Invited Talk
Logic, Complexity, and Games
- Ronald Fagin
10:00 - 10:30 Break
10:30 - 12:00 Sessions 1a and 1b
Session 1a
A General Notion of Realizability
- L. Birkedal
A Model for Impredicative Type Systems Universes,
Intersection Types and Subtyping
- Alexandre Miquel
Complete Axioms for Categorical Fixed-Point Operators
- Alex Simpson and Gordon Plotkin
Session 1b
The Role of Decidability in First Order Separations
over Classes of Finite Structures
- Steven Lindell and Scott Weinstein
Automatic Structures
- Achim Blumensath and Erich Graedel
Definability and Compression
- Foto Afrati, Hans Leiss, and Michel de Rougemont
12:00 - 1:30 Lunch
1:30 - 2:30 Sessions 2a and 2b
Session 2a
Resource-bounded Continuity and Sequentiality for
Type-Two Functionals
- Samuel R. Buss and Bruce M. Kapron
A Syntactical Analysis of Non-Size-Increasing
Polynomial Time Computation
- Klaus Aehlig and Helmut Schwichtenberg
Session 2b
Approximating Labeled Markov Processes
- Josee Desharnais, Vineet Gupta, Radha Jagadeesan,
and Prakash Panangaden
Precongruence Formats for Decorated Trace Preorders
- Bard Bloom, Wan Fokkink, and Rob van Glabbeek
2:30 - 2:45 Pause
2:45 - 4:15 Sessions 3a and 3b
Session 3a
Virtual Symmetry Reduction
- E. Allen Emerson, John W. Havlicek, and
Richard J. Trefler
Better is Better than Well:
On Efficient Verification of Infinite-State Systems
- Parosh Aziz Abdulla and Aletta Nylen
Concurrent Omega-Regular Games
- Luca de Alfaro and Thomas A. Henzinger
Session 3b
Approximate Pattern Matching is Expressible in
Transitive Closure Logic
- Kjell Lemström and Lauri Hella
Computational Complexity of Some Problems Involving
Congruences on Algebras
- Clifford Bergman and Giora Slutzki
4:15 - 4:45 Break
4:45 - 5:45 Invited Talk
From the Church-Turing Thesis to the
First-Order Algorithm Theorem
- Saul Kripke
6:30 - 8:00 Dinner
8:00 Business Meeting
TUESDAY, JUNE 27
9:00 - 10:00 Invited Talk
Satisfiability Testing: Recent Developments and
Challenge Problems
- Bart Selman
10:00 - 10:30 Break
10:30 - 12:00 Sessions 4a and 4b
Session 4a
Dominator Trees and Fast Verification of Proof Nets
- A. S. Murawski and C.-H. L. Ong
Game Semantics and Subtyping
- Juliusz Chroboczek
Probabilistic Game Semantics
- Vincent Danos and Russell Harmer
Session 4b
Back and Forth Between Guarded and Modal Logics
- Erich Graedel, Colin Hirsch, and Martin Otto
More Past Glories
- M. Reynolds
A Complete Axiomatization of Interval Temporal Logic
with Infinite Time
- B. C. Moszkowski
12:00 - 1:30 Lunch
1:30 - 2:30 Sessions 5a and 5b
Session 5a
A Modality for Recursion
- Hiroshi Nakano
A Static Calculus of Dependencies for the lambda-Cube
- Frederic Prost
Session 5b
A Decision Procedure for Term Algebras with Queues
- Tatiana Rybina and Andrei Voronkov
A Decision Procedure for the Existential Theory of
Term Algebras with a Knuth-Bendix Ordering
- Konstantin Korovin and Andrei Voronkov
2:30 - 2:45 Pause
2:45 - 3:45 Invited Talk
Some Strategies for Proving Theorems with a Model
Checker
- Ken McMillan
3:45 - 4:15 Break
4:15 - 5:52 Short Presentations
Reachability in Constraint Databases and
Model Checking for Hybrid Systems
- Michael Benedikt, Martin Grohe, Leonid Libkin,
and Luc Segoufin
Non-Commutative Logic Programming Language NoCLog
- Remi Baudot
Query Evaluation via Tree-Decompositions
- Joerg Flum, Markus Frick, and Martin Grohe
Counting with Automata
- Orna Kupferman, Amnon Ta-Shma, and Moshe Y. Vardi
Database Reformulation under Strong Storage Space Constraints
- Rada Chirkova and Michael R. Genesereth
Content-Centric Logical Environments
- Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, and
Irene Schena
About Stable Models of Non-Stratified Logic Programs
- Stefania Costantini
Systematic Design of Abstract Model Checking
- Elisa Quintarelli
Linear Logic with Polarities
- Olivier Laurent
Implementations that Preserve Confidentiality
- Jan Cederquist and Pablo Giambiagi
Arrow-Labelled Transition Systems and Modular SOS
- Peter D. Mosses
EPSL: Executable Protocol Specification Language
- Edmund Clarke, Yuan Lu, Helmut Veith, and Dong Wang
Randomized Strategy Improvement Algorithm for Parity Games
- Sergei Vorobyov
Type-Based Race Detection for Java
- Cormac Flanagan and Stephen Freund
Protocol Composition and Correctness
- Nancy Durgin, John Mitchell, Dusko Pavlovic
6:00 - 8:00 Evening beach party
WEDNESDAY, JUNE 28
9:00 - 10:00 Invited Talk
The Curry-Howard Correspondence in Set Theory
- Jean-Louis Krivine
10:00 - 10:30 Break
10:30 - 12:00 Sessions 6a and 6b
Session 6a
A Theory of Bisimulation for a Fragment of Concurrent
ML with Local Names
- Alan Jeffrey and Julian Rathke
Models for Name-Passing Processes: Interleaving and
Causal
- Gian Luca Cattani and Peter Sewell
Assigning Types to Processes
- Nobuko Yoshida and Matthew Hennessy
Session 6b
On First-Order Topological Queries
- Martin Grohe and Luc Segoufin
View-based Query Processing and Constraint
Satisfaction
- Diego Calvanese, Giuseppe De Giacomo,
Maurizio Lenzerini, and Moshe Y. Vardi
12:00 - 1:30 Lunch
1:30 - 2:30 Sessions 7a and 7b
Session 7a
Imperative Programming with Dependent Types
- Hongwei Xi
Efficient and Flexible Matching of Recursive Types
- Jens Palsberg and Tian Zhao
Session 7b
How to Optimize Proof-Search in Modal Logics:
A New Way of Proving Redundancy for Sequent Calculi
- Andrei Voronkov
Paramodulation with Built-In Abelian Groups
- Guillem Godoy and Robert Nieuwenhuis
Closing Dinner
Martin Grohe Last modified: April 3, 2000