| 2000 | A Metalanguage for Programming with Bound Names Modulo Renaming. Andrew M. Pitts, Murdoch Gabbay |
| 2000 | Formal Methods and Dependability. Cliff B. Jones |
| 2000 | Integrating Programming, Properties, and Validation. Mark P. Jones |
| 2000 | Liberating Data Refinement. Eerke A. Boiten, John Derrick |
| 2000 | Mathematics of Program Construction, 5th International Conference, MPC 2000, Ponte de Lima, Portugal, July 3-5, 2000, Proceedings Roland Carl Backhouse, José Nuno Oliveira |
| 2000 | Metacomputation-Based Compiler Architecture. William L. Harrison, Samuel N. Kamin |
| 2000 | On Guarded Commands with Fair Choice. Emil Sekerinski |
| 2000 | Polytypic Values Possess Polykinded Types. Ralf Hinze |
| 2000 | Proving Pointer Programs in Hoare Logic. Richard Bornat |
| 2000 | Quantum Programming. Jeff W. Sanders, Paolo Zuliani |
| 2000 | Reasoning about Non-terminating Loops Using Deadline Commands. Ian J. Hayes |
| 2000 | Regular Expressions Revisited: A Coinductive Approach to Streams, Automata, and Power Series. Jan J. M. M. Rutten |
| 2000 | Separation and Reduction. Ernie Cohen |
| 2000 | The Universal Resolving Algorithm: Inverse Computation in a Functional Language. Sergei M. Abramov, Robert Glück |
| 2000 | The Zip Calculus. Mark Tullsen |
| 2000 | Theorems about Composition. Michel Charpentier, K. Mani Chandy |