| 2001 | 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings |
| 2001 | A Bound on Attacks on Payment Protocols. Scott D. Stoller |
| 2001 | A Continuum of Theories of Lambda Calculus without Semantics. Antonino Salibra |
| 2001 | A Decision Procedure for an Extensional Theory of Arrays. Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy R. Levitt |
| 2001 | A Dichotomy in the Complexity of Propositional Circumscription. Lefteris M. Kirousis, Phokion G. Kolaitis |
| 2001 | A Fully Abstract Game Semantics of Local Exceptions. James Laird |
| 2001 | A Model-Theoretic Approach to Regular String Relations. Michael Benedikt, Leonid Libkin, Thomas Schwentick, Luc Segoufin |
| 2001 | A Second-Order System for Polytime Reasoning Using Graedel's Theorem. Stephen A. Cook, Antonina Kolokolova |
| 2001 | A Symbolic Labelled Transition System for Coinductive Subtyping of Alan Jeffrey |
| 2001 | A Universal Characterization of the Closed Euclidean Interval. Martín Hötzel Escardó, Alex K. Simpson |
| 2001 | An n! Lower Bound on Formula Size. Micah Adler, Neil Immerman |
| 2001 | Deconstructing Shostak. Harald Rueß, Natarajan Shankar |
| 2001 | Definitions by Rewriting in the Calculus of Constructions. Frédéric Blanqui |
| 2001 | Dependent Types for Program Termination Verification. Hongwei Xi |
| 2001 | Deterministic Generators and Games for LTL Fragments. Rajeev Alur, Salvatore La Torre |
| 2001 | Eliminating Definitions and Skolem Functions in First-Order Logic. Jeremy Avigad |
| 2001 | Focus Games for Satisfiability and Completeness of Temporal Logic. Martin Lange, Colin Stirling |
| 2001 | Foundational Proof-Carrying Code. Andrew W. Appel |
| 2001 | From Verification to Control: Dynamic Programs for Omega-Regular Objectives. Luca de Alfaro, Thomas A. Henzinger, Rupak Majumdar |
| 2001 | Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. Frank Pfenning |
| 2001 | Intuitionistic Linear Logic and Partial Correctness. Dexter Kozen, Jerzy Tiuryn |
| 2001 | Light Affine Calculus and Polytime Strong Normalization. Kazushige Terui |
| 2001 | Logician in the Land of OS: Abstract State Machines in Microsoft. Yuri Gurevich |
| 2001 | Normalization by Evaluation for Typed Lambda Calculus with Coproducts. Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip J. Scott |
| 2001 | On Definability of Order in Logic with Choice. Taneli Huuskonen, Tapani Hyttinen |
| 2001 | On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups. Guillem Godoy, Robert Nieuwenhuis |
| 2001 | On the Decision Problem for the Guarded Fragment with Transitivity. Wieslaw Szwast, Lidia Tendera |
| 2001 | Permutation Rewriting and Algorithmic Verification. Ahmed Bouajjani, Anca Muscholl, Tayssir Touili |
| 2001 | Perturbed Turing Machines and Hybrid Systems. Eugene Asarin, Ahmed Bouajjani |
| 2001 | Probabilistic Polynominal-Time Process Calculus and Security Protocol Analysis. John C. Mitchell, Ajith Ramanathan, Andre Scedrov, Vanessa Teague |
| 2001 | Relating Levels of the Mu-Calculus Hierarchy and Levels of the Monadic Hierarchy. David Janin, Giacomo Lenzi |
| 2001 | Relating Semantic and Proof-Theoretic Concepts for Polynominal Time Decidability of Uniform Word Problems. Harald Ganzinger |
| 2001 | Safety and Liveness in Branching Time. Panagiotis Manolios, Richard J. Trefler |
| 2001 | Semantics of Name and Value Passing. Marcelo P. Fiore, Daniele Turi |
| 2001 | Semistructured Data: from Practice to Theory. Serge Abiteboul |
| 2001 | Strong Normalisation in the pi-Calculus. Nobuko Yoshida, Martin Berger, Kohei Honda |
| 2001 | Successive Approximation of Abstract Transition Relations. Satyaki Das, David L. Dill |
| 2001 | Synthesizing Distributed Systems. Orna Kupferman, Moshe Y. Vardi |
| 2001 | Temporal Logic Query Checking. Glenn Bruns, Patrice Godefroid |
| 2001 | The Crane Beach Conjecture. David A. Mix Barrington, Neil Immerman, Clemens Lautemann, Nicole Schweikardt, Denis Thérien |
| 2001 | The Engineering Challenge for Logic. Wolfgang Thomas |
| 2001 | The Hierarchy inside Closed Monadic Sigma André Arnold, Giacomo Lenzi, Jerzy Marcinkowski |
| 2001 | Typechecking XML Views of Relational Databases. Noga Alon, Tova Milo, Frank Neven, Dan Suciu, Victor Vianu |