| 2001 | Deconstructing Shostak. | Harald Rue, Natarajan Shankar |
| 2001 | Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. | Frank Pfenning |
| 2001 | Probabilistic Polynominal-Time Process Calculus and Security Protocol Analysis. | John C. Mitchell, Ajith Ramanathan, Andre Scedrov, Vanessa Teague |
| 2001 | Safety and Liveness in Branching Time. | Panagiotis Manolios, Richard J. Trefler |
| 2001 | Focus Games for Satisfiability and Completeness of Temporal Logic. | Martin Lange, Colin Stirling |
| 2001 | A Fully Abstract Game Semantics of Local Exceptions. | James Laird |
| 2001 | Synthesizing Distributed Systems. | Orna Kupferman, Moshe Y. Vardi |
| 2001 | Intuitionistic Linear Logic and Partial Correctness. | Dexter Kozen, Jerzy Tiuryn |
| 2001 | A Dichotomy in the Complexity of Propositional Circumscription. | Lefteris M. Kirousis, Phokion G. Kolaitis |
| 2001 | A Symbolic Labelled Transition System for Coinductive Subtyping of | Alan Jeffrey |
| 2001 | Relating Levels of the Mu-Calculus Hierarchy and Levels of the Monadic Hierarchy. | David Janin, Giacomo Lenzi |
| 2001 | On Definability of Order in Logic with Choice. | Taneli Huuskonen, Tapani Hyttinen |
| 2001 | Logician in the Land of OS: Abstract State Machines in Microsoft. | Yuri Gurevich |
| 2001 | On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups. | Guillem Godoy, Robert Nieuwenhuis |
| 2001 | Relating Semantic and Proof-Theoretic Concepts for Polynominal Time Decidability of Uniform Word Problems. | Harald Ganzinger |
| 2001 | Semantics of Name and Value Passing. | Marcelo P. Fiore, Daniele Turi |
| 2001 | A Universal Characterization of the Closed Euclidean Interval. | Martn Htzel Escard, Alex K. Simpson |
| 2001 | Successive Approximation of Abstract Transition Relations. | Satyaki Das, David L. Dill |
| 2001 | A Second-Order System for Polytime Reasoning Using Graedel's Theorem. | Stephen A. Cook, Antonina Kolokolova |
| 2001 | Temporal Logic Query Checking. | Glenn Bruns, Patrice Godefroid |
| 2001 | Permutation Rewriting and Algorithmic Verification. | Ahmed Bouajjani, Anca Muscholl, Tayssir Touili |
| 2001 | Definitions by Rewriting in the Calculus of Constructions. | Frdric Blanqui |
| 2001 | A Model-Theoretic Approach to Regular String Relations. | Michael Benedikt, Leonid Libkin, Thomas Schwentick, Luc Segoufin |
| 2001 | The Crane Beach Conjecture. | David A. Mix Barrington, Neil Immerman, Clemens Lautemann, Nicole Schweikardt, Denis Thrien |
| 2001 | Eliminating Definitions and Skolem Functions in First-Order Logic. | Jeremy Avigad |