| 2009 | A model of cooperative threads. | Martn Abadi, Gordon D. Plotkin |
| 2008 | Demand-driven alias analysis for C. | Xin Zheng, Radu Rugina |
| 2008 | Focusing and higher-order abstract syntax. | Noam Zeilberger |
| 2008 | Generating precise and concise procedure summaries. | Greta Yorsh, Eran Yahav, Satish Chandra |
| 2008 | Much ado about two (pearl): a pearl on parallel prefix computation. | Janis Voigtlnder |
| 2008 | Automatic inference of stationary fields: a generalization of java's final fields. | Christopher Unkel, Monica S. Lam |
| 2008 | Formal verification of translation validators: a case study on instruction scheduling optimizations. | Jean-Baptiste Tristan, Xavier Leroy |
| 2008 | The design and implementation of typed scheme. | Sam Tobin-Hochstadt, Matthias Felleisen |
| 2008 | A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. | Brigitte Pientka |
| 2008 | Separation logic, abstraction and inheritance. | Matthew J. Parkinson, Gavin M. Bierman |
| 2008 | A theory of platform-dependent low-level software. | Marius Nita, Dan Grossman, Craig Chambers |
| 2008 | Contextual effects for version-consistent dynamic software updatingalland safe concurrent programming. | Iulian Neamtiu, Michael Hicks, Jeffrey S. Foster, Polyvios Pratikakis |
| 2008 | High-level small-step operational semantics for transactions. | Katherine F. Moore, Dan Grossman |
| 2008 | Caml trading. | Yaron Minsky |
| 2008 | Relevance heuristics for program analysis. | Kenneth L. McMillan |
| 2008 | Clowns to the left of me, jokers to the right (pearl): dissecting data structures. | Conor McBride |
| 2008 | On the computational soundness of cryptographically masked flows. | Peeter Laud |
| 2008 | Back to the future: revisiting precise program verification using SMT solvers. | Shuvendu K. Lahiri, Shaz Qadeer |
| 2008 | Foundations for structured programming with GADTs. | Patricia Johann, Neil Ghani |
| 2008 | Multiparty asynchronous session types. | Kohei Honda, Nobuko Yoshida, Marco Carbone |
| 2008 | An approach to call-by-name delimited continuations. | Hugo Herbelin, Silvia Ghilezan |
| 2008 | Proving non-termination. | Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, Ru-Gang Xu |
| 2008 | Lifting abstract interpreters to quantified logical domains. | Sumit Gulwani, Bill McCloskey, Ashish Tiwari |
| 2008 | A logical account of pspace. | Marco Gaboardi, Jean-Yves Marion, Simona Ronchi Della Rocca |
| 2008 | Cryptographically sound implementations for typed information-flow security. | Cdric Fournet, Tamara Rezk |