| 2009 | Types and higher-order recursion schemes for verification of higher-order programs. | Naoki Kobayashi |
| 2009 | Positive supercompilation for a higher order call-by-value language. | Peter A. Jonsson, Johan Nordlander |
| 2009 | Controlling chaos: on safe side-effects in data-parallel operations. | Stephan Herhut, Sven-Bodo Scholz, Clemens Grelck |
| 2009 | Automated verification of practical garbage collectors. | Chris Hawblitzel, Erez Petrank |
| 2009 | Language constructs for transactional memory. | Tim Harris |
| 2009 | Semi-sparse flow-sensitive pointer analysis. | Ben Hardekopf, Calvin Lin |
| 2009 | SPEED: precise and efficient static estimation of program computational complexity. | Sumit Gulwani, Krishna K. Mehra, Trishul M. Chilimbi |
| 2009 | A combination framework for tracking partition sizes. | Sumit Gulwani, Tal Lev-Ami, Mooly Sagiv |
| 2009 | The semantics of progress in lock-based transactional memory. | Rachid Guerraoui, Michal Kapalka |
| 2009 | Proving that non-blocking algorithms don't block. | Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis |
| 2009 | Lazy evaluation and delimited control. | Ronald Garcia, Andrew Lumsdaine, Amr Sabry |
| 2009 | Verifying liveness for asynchronous programs. | Pierre Ganty, Rupak Majumdar, Andrey Rybalchenko |
| 2009 | Local rely-guarantee reasoning. | Xinyu Feng |
| 2009 | A calculus of atomic actions. | Tayfun Elmas, Shaz Qadeer, Serdar Tasiran |
| 2009 | Unifying type checking and property checking for low-level code. | Jeremy Condit, Brian Hackett, Shuvendu K. Lahiri, Shaz Qadeer |
| 2009 | Compositional shape analysis by means of bi-abduction. | Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang |
| 2009 | Declarative aspects of memory management in the concurrent collections parallel programming model. | Zoran Budimlic, Aparna Chandramowlishwaran, Kathleen Knobe, Geoff N. Lowney, Vivek Sarkar, Leo Treggiari |
| 2009 | A foundation for flow-based program matching: using temporal logic and model checking. | Julien Brunel, Damien Doligez, Ren Rydhof Hansen, Julia L. Lawall, Gilles Muller |
| 2009 | Classical BI: a logic for reasoning about dualising resources. | James Brotherston, Cristiano Calcagno |
| 2009 | Feedback-directed barrier optimization in a strongly isolated STM. | Nathan Grasso Bronson, Christos Kozyrakis, Kunle Olukotun |
| 2009 | Relaxed memory models: an operational approach. | Grard Boudol, Gustavo Petri |
| 2009 | Formal certification of code-based cryptographic proofs. | Gilles Barthe, Benjamin Grgoire, Santiago Zanella-Bguelin |
| 2009 | Wild control operators. | Chris Barker |
| 2009 | The semantics of power and ARM multiprocessor machine code. | Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli |
| 2009 | State-dependent representation independence. | Amal Ahmed, Derek Dreyer, Andreas Rossberg |