LICS 2000 Call for Participation and Preliminary Program

        	  Fifteenth Annual IEEE Symposium on 
	    June  26 - 28, 2000, Santa Barbara, California



The LICS Symposium is an annual international forum on theoretical and
practical topics in computer science that relate to logic in a broad

LICS 2000 Invited Speakers are

	  Ronald Fagin (IBM Almaden Research Center)
	  Saul Kripke (Princeton University)
	  Jean-Louis Krivine (University of Paris 7)
	  Ken McMillan (Cadence)
	  Bart Selman (Cornell University).

A prelimary program can be found below.

LICS 2000 Registration and Conference Information is now available on
the LICS website:




LICS 2000 Preliminary Program

Monday, June 26

 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

 9: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
               - Ken McMillan

 3:45 - 4:15   Break

 4:15          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

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

End of LICS, start of Tutorial Workshop on Proof-Carrying Code