15. LICS 2000: Santa Barbara, California, USA

Invited Talk

• Ronald Fagin:
  Logic, Complexity, and Games. 3
  

Session 1a

• Lars Birkedal:
  A General Notion of Realizability. 7-17
  
• Alexandre Miquel:
  A Model for Impredicative Type Systems, Universes, Intersection Types and Subtyping. 18-29
  
• Alex K. Simpson, Gordon D. Plotkin:
  Complete Axioms for Categorical Fixed-Point Operators. 30-41
  

Session 1b

• Steven Lindell, Scott Weinstein:
  The Role of Decidability in First Order Separations over Classes of Finite Structures. 45-50
  
• Achim Blumensath, Erich Grädel:
  Automatic Structures. 51-62
  
• Foto N. Afrati, Hans Leiß, Michel de Rougemont:
  Definability and Compression. 63-73
  

Session 2a

• Samuel R. Buss, Bruce M. Kapron:
  Resource-Bounded Continuity and Sequentiality for Type-Two Functionals. 77-83
  
• Klaus Aehlig, Helmut Schwichtenberg:
  A Syntactical Analysis of Non-Size-Increasing Polynomial Time Computation. 84-91
  

Session 2b

• Josee Desharnais, Vineet Gupta, Radha Jagadeesan, Prakash Panangaden:
  Approximating Labeled Markov Processes. 95-106
  
• Bard Bloom, Wan Fokkink, Rob J. van Glabbeek:
  Precongruence Formats for Decorated Trace Preorders. 107-118
  

Session 3a

• E. Allen Emerson, John Havlicek, Richard J. Trefler:
  Virtual Symmetry Reduction. 121-131
  
• Parosh Aziz Abdulla, Aletta Nylén:
  Better is Better than Well: On Efficient Verification of Infinite-State Systems. 132-140
  
• Luca de Alfaro, Thomas A. Henzinger:
  Concurrent Omega-Regular Games. 141-154
  

Session 3b

• Kjell Lemström, Lauri Hella:
  Approximate Pattern Matching is Expressible in Transitive Closure Logic. 157-167
  
• Clifford Bergman, Giora Slutzki:
  Computational Complexity of Some Problems Involving Congruences on Algebras. 168-174
  

Invited Talks

• Saul Kripke:
  From the Church-Turing Thesis to the First-Order Algorithm Theorem. 177
  
• Bart Selman:
  Satisfiability Testing: Recent Developments and Challenge Problems. 178
  

Session 4a

• Andrzej S. Murawski, C.-H. Luke Ong:
  Dominator Trees and Fast Verification of Proof Nets. 181-191
  
• Juliusz Chroboczek:
  Game Semantics and Subtyping. 192-203
  
• Vincent Danos, Russell Harmer:
  Probabilistic Game Semantics. 204-213
  

Session 4b

• Erich Grädel, Colin Hirsch, Martin Otto:
  Back and Forth between Guarded and Modal Logics. 217-228
  
• Mark Reynolds:
  More Past Glories. 229-240
  
• Ben C. Moszkowski:
  A Complete Axiomatization of Interval Temporal Logic with Infinite Time. 241-252
  

Session 5a

• Hiroshi Nakano:
  A Modality for Recursion. 255-266
  
• Frédéric Prost:
  A Static Calculus of Dependencies for the lambda-Cube. 267-276
  

Session 5b

• Tatiana Rybina, Andrei Voronkov:
  A Decision Procedure for Term Algebras with Queues. 279-290
  
• Konstantin Korovin, Andrei Voronkov:
  A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering. 291-302
  

Invited Talks

• Kenneth L. McMillan:
  Some Strategies for Proving Theorems with a Model Checker. 305-306
  
• Jean-Louis Krivine:
  The Curry-Howard Correspondence in Set Theory. 307-308
  

Session 6a

• Alan Jeffrey, Julian Rathke:
  A Theory of Bisimulation for a Fragment of Concurrent ML with Local Names. 311-321
  
• Gian Luca Cattani, Peter Sewell:
  Models for Name-Passing Processes: Interleaving and Causal. 322-332
  
• Nobuko Yoshida, Matthew Hennessy:
  Assigning Types to Processes. 334-345
  

Session 6b

• Martin Grohe, Luc Segoufin:
  On First-Order Topological Queries. 349-360
  
• Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi:
  View-Based Query Processing and Constraint Satisfaction. 361-371
  

Session 7a

• Hongwei Xi:
  Imperative Programming with Dependent Types. 375-387
  
• Jens Palsberg, Tian Zhao:
  Efficient and Flexible Matching of Recursive Types. 388-398
  

Session 7b

• Andrei Voronkov:
  How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi. 401-412
  
• Guillem Godoy, Robert Nieuwenhuis:
  Paramodulation with Built-in Abelian Groups. 413-424