| 2000 | A Fully Complete PER Model for ML Polymorphic Types. Samson Abramsky, Marina Lenisa |
| 2000 | A Theory of Explicit Mathematics Equivalent to ID Reinhard Kahle, Thomas Studer |
| 2000 | Automated Verification = Graphs, Automata, and Logic. Moshe Y. Vardi |
| 2000 | Axiomatizing the Least Fixed Point Operation and Binary Supremum. Zoltán Ésik |
| 2000 | Background, Reserve, and Gandy Machines. Andreas Blass, Yuri Gurevich |
| 2000 | Bounded Arithmetic and Descriptive Complexity. Achim Blumensath |
| 2000 | Choiceless Polynominal Time Computation and the Zero-One Law. Andreas Blass, Yuri Gurevich |
| 2000 | Choiceless Polynominal Time Logic: Inability to Express. Saharon Shelah |
| 2000 | Completeness of Higher-Order Duration Calculus. Naijun Zhan |
| 2000 | Composition and Submachine Concepts for Sequential ASMs. Egon Börger, Joachim Schmid |
| 2000 | Computer Science Logic, 14th Annual Conference of the EACSL, Fischbachau, Germany, August 21-26, 2000, Proceedings Peter Clote, Helmut Schwichtenberg |
| 2000 | Continuous Functionals of Dependent Types and Equilogical Spaces. Andrej Bauer, Lars Birkedal |
| 2000 | Definability over Linear Constraints. Michael Benedikt, H. Jerome Keisler |
| 2000 | Discreet Games, Light Affine Logic and PTIME Computation. Andrzej S. Murawski, C.-H. Luke Ong |
| 2000 | Disjunctive Tautologies as Synchronisation Schemes. Vincent Danos, Jean-Louis Krivine |
| 2000 | Elementary Choiceless Constructive Analysis. Peter M. Schuster |
| 2000 | Elimination of Negation in a Logical Framework. Alberto Momigliano |
| 2000 | Equational Termination by Semantic Labelling. Hitoshi Ohsaki, Aart Middeldorp, Jürgen Giesl |
| 2000 | Finite Models and Full Completeness. James Laird |
| 2000 | Flatness Is Not a Weakness. Hubert Comon, Véronique Cortier |
| 2000 | From Programs to Games: Invariance and Safety for Bisimulation. Marc Pauly |
| 2000 | Hypersequent and the Proof Theory of Intuitionistic Fuzzy Logic. Matthias Baaz, Richard Zach |
| 2000 | Independence: Logics and Concurrency. Julian C. Bradfield |
| 2000 | Interactive Programs in Dependent Type Theory. Peter G. Hancock, Anton Setzer |
| 2000 | Logic Programming and Co-inductive Definitions. Mathieu Jaume |
| 2000 | Logical Relations and Data Abstraction. John Power, Edmund Robinson |
| 2000 | Modal Satisfiability Is in Deterministic Linear Space. Edith Hemaspaandra |
| 2000 | On the Complexity of Combinatorial and Metafinite Generating Functions of Graph Properties in the Computational Model of Blum, Shub and Smale. Johann A. Makowsky, Klaus Meer |
| 2000 | On the Complexity of Explicit Modal Logics. Roman Kuznets |
| 2000 | On the Computational Interpretation of Negation. Michel Parigot |
| 2000 | On the Logic of the Standard Proof Predicate. Rostislav E. Yavorsky |
| 2000 | Schema Revisited. Colin Stirling |
| 2000 | Sequents, Frames, and Completeness. Thierry Coquand, Guo-Qiang Zhang |
| 2000 | Subtyping with Power Types. David Aspinall |
| 2000 | The Descriptive Comlexity of the Fixed-Points of Bounded Formulas. Albert Atserias |
| 2000 | Translating Theory into Practice - Abstract State Machines within Microsoft. Wolfram Schulte |
| 2000 | Une tentative malheureuse do construire une structure éliminant rapidement les quanteurs. Bruno Poizat |