| 2000 | A Higher-Order Simulation Relation for System F. Jo Erskine Hannay |
| 2000 | A Program Refinement Framework Supporting Reasoning about Knowledge and Time. Kai Engelhardt, Ron van der Meyden, Yoram Moses |
| 2000 | A Proof System for Timed Automata. Huimin Lin, Wang Yi |
| 2000 | An Algebraic Foundation for Adaptive Programming. Peter Thiemann |
| 2000 | Categorical Models for Intuitionistic and Linear Type Theory. Maria Emilia Maietti, Valeria de Paiva, Eike Ritter |
| 2000 | Compositional Verification in Linear-Time Temporal Logic. Yih-Kuen Tsay |
| 2000 | Constructive Data Refinement in Typed Lambda Calculus. Furio Honsell, John Longley, Donald Sannella, Andrzej Tarlecki |
| 2000 | Constructor Subtyping in the Calculus of Inductive Constructions. Gilles Barthe, Femke van Raamsdonk |
| 2000 | Foundations of Software Science and Computation Structures, Third International Conference, FOSSACS 2000, Held as Part of the Joint European Conferences on Theory and Practice of Software,ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings Jerzy Tiuryn |
| 2000 | Hierarchical Graph Transformation. Frank Drewes, Berthold Hoffmann, Detlef Plump |
| 2000 | Locality and Polyadicity in Asynchronous Name-Passing Calculi. Massimo Merro |
| 2000 | Norm Functions for Probabilistic Bisimulations with Delays. Christel Baier, Mariëlle Stoelinga |
| 2000 | On Rational Graphs. Christophe Morvan |
| 2000 | On Recognizable Stable Trace Languages. Jean-François Husson, Rémi Morin |
| 2000 | On Synchronous and Asynchronous Mobile Processes. Paola Quaglia, David Walker |
| 2000 | On Word Rewriting Systems Having a Rational Derivation. Didier Caucal |
| 2000 | On the Semantics of Refinement Calculi. Hongseok Yang, Uday S. Reddy |
| 2000 | Predicate Logic and Tree Automata with Tests. Ralf Treinen |
| 2000 | Probabilistic Asynchronous pi-Calculus. Oltea Mihaela Herescu, Catuscia Palamidessi |
| 2000 | Proof Nets and Explicit Substitutions. Roberto Di Cosmo, Delia Kesner, Emmanuel Polonowski |
| 2000 | Sequential and Concurrent Abstract Machines for Interaction Nets. Jorge Sousa Pinto |
| 2000 | Subtyping and Typing Algorithms for Mobile Ambients. Pascal Zimmer |
| 2000 | The State Explosion Problem from Trace to Bisimulation Equivalence. François Laroussinie, Philippe Schnoebelen |
| 2000 | Type Inference for First-Order Logic. Aleksy Schubert |
| 2000 | Typing Local Definitions and Conditional Expressions with Rank 2 Intersection. Ferruccio Damiani |
| 2000 | Verifying Performance Equivalence for Timed Basic Parallel Processes. Béatrice Bérard, Anne Labroue, Philippe Schnoebelen |