| 2001 | Perturbed Turing Machines and Hybrid Systems. | Eugene Asarin, Ahmed Bouajjani |
| 2001 | The Hierarchy inside Closed Monadic Sigma | Andr Arnold, Giacomo Lenzi, Jerzy Marcinkowski |
| 2001 | Foundational Proof-Carrying Code. | Andrew W. Appel |
| 2001 | Deterministic Generators and Games for LTL Fragments. | Rajeev Alur, Salvatore La Torre |
| 2001 | Normalization by Evaluation for Typed Lambda Calculus with Coproducts. | Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip J. Scott |
| 2001 | Typechecking XML Views of Relational Databases. | Noga Alon, Tova Milo, Frank Neven, Dan Suciu, Victor Vianu |
| 2001 | From Verification to Control: Dynamic Programs for Omega-Regular Objectives. | Luca de Alfaro, Thomas A. Henzinger, Rupak Majumdar |
| 2001 | An n! Lower Bound on Formula Size. | Micah Adler, Neil Immerman |
| 2001 | Semistructured Data: from Practice to Theory. | Serge Abiteboul |
| 2000 | Assigning Types to Processes. | Nobuko Yoshida, Matthew Hennessy |
| 2000 | Imperative Programming with Dependent Types. | Hongwei Xi |
| 2000 | How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi. | Andrei Voronkov |
| 2000 | Complete Axioms for Categorical Fixed-Point Operators. | Alex K. Simpson, Gordon D. Plotkin |
| 2000 | Satisfiability Testing: Recent Developments and Challenge Problems. | Bart Selman |
| 2000 | A Decision Procedure for Term Algebras with Queues. | Tatiana Rybina, Andrei Voronkov |
| 2000 | More Past Glories. | Mark Reynolds |
| 2000 | A Static Calculus of Dependencies for the lambda-Cube. | Frdric Prost |
| 2000 | Efficient and Flexible Matching of Recursive Types. | Jens Palsberg, Tian Zhao |
| 2000 | A Modality for Recursion. | Hiroshi Nakano |
| 2000 | Dominator Trees and Fast Verification of Proof Nets. | Andrzej S. Murawski, C.-H. Luke Ong |
| 2000 | A Complete Axiomatization of Interval Temporal Logic with Infinite Time. | Ben C. Moszkowski |
| 2000 | A Model for Impredicative Type Systems, Universes, Intersection Types and Subtyping. | Alexandre Miquel |
| 2000 | Some Strategies for Proving Theorems with a Model Checker. | Kenneth L. McMillan |
| 2000 | The Role of Decidability in First Order Separations over Classes of Finite Structures. | Steven Lindell, Scott Weinstein |
| 2000 | Approximate Pattern Matching is Expressible in Transitive Closure Logic. | Kjell Lemstrm, Lauri Hella |