| 2009 | A calculus of atomic actions. Tayfun Elmas, Shaz Qadeer, Serdar Tasiran |
| 2009 | A combination framework for tracking partition sizes. Sumit Gulwani, Tal Lev-Ami, Mooly Sagiv |
| 2009 | A cost semantics for self-adjusting computation. Ruy Ley-Wild, Umut A. Acar, Matthew Fluet |
| 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 | A model of cooperative threads. Martín Abadi, Gordon D. Plotkin |
| 2009 | Automated verification of practical garbage collectors. Chris Hawblitzel, Erez Petrank |
| 2009 | Automatic modular abstractions for linear constraints. David Monniaux |
| 2009 | Bidirectionalization for free! (Pearl). Janis Voigtländer |
| 2009 | Classical BI: a logic for reasoning about dualising resources. James Brotherston, Cristiano Calcagno |
| 2009 | Compositional shape analysis by means of bi-abduction. Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang |
| 2009 | Copy-on-write in the PHP language. Akihiko Tozawa, Michiaki Tatsubori, Tamiya Onodera, Yasuhiko Minamide |
| 2009 | Equality saturation: a new approach to optimization. Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner |
| 2009 | Feedback-directed barrier optimization in a strongly isolated STM. Nathan Grasso Bronson, Christos Kozyrakis, Kunle Olukotun |
| 2009 | Flexible types: robust type inference for first-class polymorphism. Daan Leijen |
| 2009 | Focusing on pattern matching. Neelakantan R. Krishnaswami |
| 2009 | Formal certification of code-based cryptographic proofs. Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin |
| 2009 | Language constructs for transactional memory. Tim Harris |
| 2009 | Lazy evaluation and delimited control. Ronald Garcia, Andrew Lumsdaine, Amr Sabry |
| 2009 | Linear types for computational effects. Alex Simpson |
| 2009 | Local rely-guarantee reasoning. Xinyu Feng |
| 2009 | Masked types for sound object initialization. Xin Qi, Andrew C. Myers |
| 2009 | Modeling abstract types in modules with open existential types. Benoît Montagu, Didier Rémy |
| 2009 | Modular code generation from synchronous block diagrams: modularity vs. code size. Roberto Lublinerman, Christian Szegedy, Stavros Tripakis |
| 2009 | Positive supercompilation for a higher order call-by-value language. Peter A. Jonsson, Johan Nordlander |
| 2009 | Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009 Zhong Shao, Benjamin C. Pierce |
| 2009 | Proving that non-blocking algorithms don't block. Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis |
| 2009 | Relaxed memory models: an operational approach. Gérard Boudol, Gustavo Petri |
| 2009 | SPEED: precise and efficient static estimation of program computational complexity. Sumit Gulwani, Krishna K. Mehra, Trishul M. Chilimbi |
| 2009 | Semi-sparse flow-sensitive pointer analysis. Ben Hardekopf, Calvin Lin |
| 2009 | State-dependent representation independence. Amal Ahmed, Derek Dreyer, Andreas Rossberg |
| 2009 | Static contract checking for Haskell. Dana N. Xu, Simon L. Peyton Jones, Koen Claessen |
| 2009 | The semantics of progress in lock-based transactional memory. Rachid Guerraoui, Michal Kapalka |
| 2009 | The semantics of x86-CC multiprocessor machine code. Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, Jade Alglave |
| 2009 | The theory of deadlock avoidance via discrete control. Yin Wang, Stéphane Lafortune, Terence Kelly, Manjunath Kudlur, Scott A. Mahlke |
| 2009 | The third homomorphism theorem on trees: downward & upward lead to divide-and-conquer. Akimasa Morihata, Kiminori Matsuzaki, Zhenjiang Hu, Masato Takeichi |
| 2009 | Types and higher-order recursion schemes for verification of higher-order programs. Naoki Kobayashi |
| 2009 | Unifying type checking and property checking for low-level code. Jeremy Condit, Brian Hackett, Shuvendu K. Lahiri, Shaz Qadeer |
| 2009 | Verifying distributed systems: the operational approach. Tom Ridge |
| 2009 | Verifying liveness for asynchronous programs. Pierre Ganty, Rupak Majumdar, Andrey Rybalchenko |
| 2009 | Wild control operators. Chris Barker |