| 2005 | A bisimulation for type abstraction and recursion. Eijiro Sumii, Benjamin C. Pierce |
| 2005 | A framework for numeric analysis of array operations. Denis Gopan, Thomas W. Reps, Shmuel Sagiv |
| 2005 | A probabilistic language based upon sampling functions. Sungwoo Park, Frank Pfenning, Sebastian Thrun |
| 2005 | A semantics for procedure local heaps and its abstractions. Noam Rinetzky, Jörg Bauer, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm |
| 2005 | A simple typed intermediate language for object-oriented languages. Juan Chen, David Tarditi |
| 2005 | A syntactic approach to eta equality in type theory. Healfdene Goguen |
| 2005 | Associated types with class. Manuel M. T. Chakravarty, Gabriele Keller, Simon L. Peyton Jones, Simon Marlow |
| 2005 | Automated soundness proofs for dataflow analyses and transformations via local rules. Sorin Lerner, Todd D. Millstein, Erika Rice, Craig Chambers |
| 2005 | Combinators for bi-directional tree transformations: a linguistic approach to the view update problem. J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, Alan Schmitt |
| 2005 | Communicating quantum processes. Simon J. Gay, Rajagopal Nagarajan |
| 2005 | Connecting effects and uniqueness with adoption. John Tang Boyland, William Retert |
| 2005 | Context logic and tree update. Cristiano Calcagno, Philippa Gardner, Uri Zarfaty |
| 2005 | Downgrading policies and relaxed noninterference. Peng Li, Steve Zdancewic |
| 2005 | Dynamic partial-order reduction for model checking software. Cormac Flanagan, Patrice Godefroid |
| 2005 | Environmental acquisition revisited. Richard Cobbe, Matthias Felleisen |
| 2005 | From sequential programs to multi-tier applications by program transformation. Matthias Neubauer, Peter Thiemann |
| 2005 | Mutatis mutandis: safe and predictable dynamic software updating. Gareth Paul Stoyle, Michael W. Hicks, Gavin M. Bierman, Peter Sewell, Iulian Neamtiu |
| 2005 | Parametric polymorphism for XML. Haruo Hosoya, Alain Frisch, Giuseppe Castagna |
| 2005 | Permission accounting in separation logic. Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, Matthew J. Parkinson |
| 2005 | Polymorphic bytecode: compositional compilation for Java-like languages. Davide Ancona, Ferruccio Damiani, Sophia Drossopoulou, Elena Zucca |
| 2005 | Precise interprocedural analysis using random interpretation. Sumit Gulwani, George C. Necula |
| 2005 | Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005 Jens Palsberg, Martín Abadi |
| 2005 | Proof-guided underapproximation-widening for multi-process systems. Orna Grumberg, Flavio Lerda, Ofer Strichman, Michael Theobald |
| 2005 | Region-based shape analysis with tracked locations. Brian Hackett, Radu Rugina |
| 2005 | Scalable error detection using boolean satisfiability. Yichen Xie, Alex Aiken |
| 2005 | Separation logic and abstraction. Matthew J. Parkinson, Gavin M. Bierman |
| 2005 | Slot games: a quantitative model of computation. Dan R. Ghica |
| 2005 | Synthesis of interface specifications for Java classes. Rajeev Alur, Pavol Cerný, P. Madhusudan, Wonhong Nam |
| 2005 | The Java memory model. Jeremy Manson, William W. Pugh, Sarita V. Adve |
| 2005 | Theoretical foundations for compensations in flow composition languages. Roberto Bruni, Hernán C. Melgratti, Ugo Montanari |
| 2005 | Transactors: a programming model for maintaining globally consistent distributed state in unreliable environments. John Field, Carlos A. Varela |
| 2005 | Transition predicate abstraction and fair termination. Andreas Podelski, Andrey Rybalchenko |