| 2000 | (Optimal) Duplication is not Elementary Recursive. Andrea Asperti, Paolo Coppola, Simone Martini |
| 2000 | A Debate on Language and Tool Support for Design Patterns. Craig Chambers, Bill Harrison, John M. Vlissides |
| 2000 | A Framework for Combining Analysis and Verification. Nevin Heintze, Joxan Jaffar, Razvan Voicu |
| 2000 | A New Approach to Generic Functional Programming. Ralf Hinze |
| 2000 | A Semantic Model of Types and Machine Instructions for Proof-Carrying Code. Andrew W. Appel, Amy P. Felty |
| 2000 | A Type System for Dynamic Web Documents. Anders Sandholm, Michael I. Schwartzbach |
| 2000 | A Type System for Expressive Security Policies. David Walker |
| 2000 | Analytic Constraint Solving and Interval Arithmetic. Timothy J. Hickey |
| 2000 | Anytime, Anywhere: Modal Logics for Mobile Ambients. Luca Cardelli, Andrew D. Gordon |
| 2000 | Authentication Primitives and Their Compilation. Martín Abadi, Cédric Fournet, Georges Gonthier |
| 2000 | Controlling Interference in Ambients. Francesca Levi, Davide Sangiorgi |
| 2000 | Deciding Type Equivalence with Singleton Kinds. Christopher A. Stone, Robert Harper |
| 2000 | Efficient Algorithms for pre Javier Esparza, Andreas Podelski |
| 2000 | Enforcing Trace Properties by Program Transformation. Thomas Colcombet, Pascal Fradet |
| 2000 | First-Class Macros have Types. Alan Bawden |
| 2000 | Generalized Certificate Revocation. Carl A. Gunter, Trevor Jim |
| 2000 | Implicit Parameters: Dynamic Scoping with Static Types. Jeffrey R. Lewis, John Launchbury, Erik Meijer, Mark Shields |
| 2000 | Modular Refinement of Hierarchic Reactive Machines. Rajeev Alur, Radu Grosu |
| 2000 | On the Complexity of Flow-Sensitive Dataflow Analyses. Robert Muth, Saumya K. Debray |
| 2000 | POPL 2000, Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts, USA, January 19-21, 2000 Mark N. Wegman, Thomas W. Reps |
| 2000 | Paths vs. Trees in Set-Based Program Analysis. Witold Charatonik, Andreas Podelski, Jean-Marc Talbot |
| 2000 | Projection Merging: Reducing Redundancies in Inclusion Constraint Graphs. Zhendong Su, Manuel Fähndrich, Alexander Aiken |
| 2000 | Reducing Sweep Time for a Nearly Empty Heap. Yoo C. Chung, Soo-Mook Moon, Kemal Ebcioglu, Dan Sahlin |
| 2000 | Resource Bound Certification. Karl Crary, Stephanie Weirich |
| 2000 | Semantics-Preserving Procedure Extraction. Raghavan Komondoor, Susan Horwitz |
| 2000 | Shape Analysis for Mobile Ambients. Hanne Riis Nielson, Flemming Nielson |
| 2000 | Sparse Code Motion. Oliver Rüthing, Jens Knoop, Bernhard Steffen |
| 2000 | Temporal Abstract Interpretation. Patrick Cousot, Radhia Cousot |
| 2000 | Transforming Out Timing Leaks. Johan Agat |
| 2000 | Type Elaboration and Subtype Completion for Java Bytecode. Todd B. Knoblock, Jakob Rehof |
| 2000 | Type Systems for Distributed Data Structures. Ben Liblit, Alexander Aiken |
| 2000 | Verifying Secrets and Relative Secrecy. Dennis M. Volpano, Geoffrey Smith |