| 2000 | 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, California, USA, June 26-29, 2000 |
| 2000 | A Complete Axiomatization of Interval Temporal Logic with Infinite Time. Ben C. Moszkowski |
| 2000 | A Decision Procedure for Term Algebras with Queues. Tatiana Rybina, Andrei Voronkov |
| 2000 | A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering. Konstantin Korovin, Andrei Voronkov |
| 2000 | A General Notion of Realizability. Lars Birkedal |
| 2000 | A Modality for Recursion. Hiroshi Nakano |
| 2000 | A Model for Impredicative Type Systems, Universes, Intersection Types and Subtyping. Alexandre Miquel |
| 2000 | A Static Calculus of Dependencies for the lambda-Cube. Frédéric Prost |
| 2000 | A Syntactical Analysis of Non-Size-Increasing Polynomial Time Computation. Klaus Aehlig, Helmut Schwichtenberg |
| 2000 | A Theory of Bisimulation for a Fragment of Concurrent ML with Local Names. Alan Jeffrey, Julian Rathke |
| 2000 | Approximate Pattern Matching is Expressible in Transitive Closure Logic. Kjell Lemström, Lauri Hella |
| 2000 | Approximating Labeled Markov Processes. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, Prakash Panangaden |
| 2000 | Assigning Types to Processes. Nobuko Yoshida, Matthew Hennessy |
| 2000 | Automatic Structures. Achim Blumensath, Erich Grädel |
| 2000 | Back and Forth between Guarded and Modal Logics. Erich Grädel, Colin Hirsch, Martin Otto |
| 2000 | Better is Better than Well: On Efficient Verification of Infinite-State Systems. Parosh Aziz Abdulla, Aletta Nylén |
| 2000 | Complete Axioms for Categorical Fixed-Point Operators. Alex K. Simpson, Gordon D. Plotkin |
| 2000 | Computational Complexity of Some Problems Involving Congruences on Algebras. Clifford Bergman, Giora Slutzki |
| 2000 | Concurrent Omega-Regular Games. Luca de Alfaro, Thomas A. Henzinger |
| 2000 | Definability and Compression. Foto N. Afrati, Hans Leiß, Michel de Rougemont |
| 2000 | Dominator Trees and Fast Verification of Proof Nets. Andrzej S. Murawski, C.-H. Luke Ong |
| 2000 | Efficient and Flexible Matching of Recursive Types. Jens Palsberg, Tian Zhao |
| 2000 | From the Church-Turing Thesis to the First-Order Algorithm Theorem. Saul Kripke |
| 2000 | Game Semantics and Subtyping. Juliusz Chroboczek |
| 2000 | How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi. Andrei Voronkov |
| 2000 | Imperative Programming with Dependent Types. Hongwei Xi |
| 2000 | Logic, Complexity, and Games. Ronald Fagin |
| 2000 | Models for Name-Passing Processes: Interleaving and Causal. Gian Luca Cattani, Peter Sewell |
| 2000 | More Past Glories. Mark Reynolds |
| 2000 | On First-Order Topological Queries. Martin Grohe, Luc Segoufin |
| 2000 | Paramodulation with Built-in Abelian Groups. Guillem Godoy, Robert Nieuwenhuis |
| 2000 | Precongruence Formats for Decorated Trace Preorders. Bard Bloom, Wan J. Fokkink, Rob J. van Glabbeek |
| 2000 | Probabilistic Game Semantics. Vincent Danos, Russell Harmer |
| 2000 | Resource-Bounded Continuity and Sequentiality for Type-Two Functionals. Samuel R. Buss, Bruce M. Kapron |
| 2000 | Satisfiability Testing: Recent Developments and Challenge Problems. Bart Selman |
| 2000 | Some Strategies for Proving Theorems with a Model Checker. Kenneth L. McMillan |
| 2000 | The Curry-Howard Correspondence in Set Theory. Jean-Louis Krivine |
| 2000 | The Role of Decidability in First Order Separations over Classes of Finite Structures. Steven Lindell, Scott Weinstein |
| 2000 | View-Based Query Processing and Constraint Satisfaction. Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi |
| 2000 | Virtual Symmetry Reduction. E. Allen Emerson, John Havlicek, Richard J. Trefler |