| 2012 | Programming languages for programmable networks. | Jennifer Rexford |
| 2012 | Syntactic control of interference for separation logic. | Uday S. Reddy, John C. Reynolds |
| 2012 | Defining code-injection attacks. | Donald Ray, Jay Ligatti |
| 2012 | The ins and outs of gradual type inference. | Aseem Rastogi, Avik Chaudhuri, Basil Hosmer |
| 2012 | A mechanized semantics for C++ object construction and destruction, with applications to resource management. | Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy |
| 2012 | Abstractions from tests. | Mayur Naik, Hongseok Yang, Ghila Castelnuovo, Mooly Sagiv |
| 2012 | A type system for borrowing permissions. | Karl Naden, Robert Bocchino, Jonathan Aldrich, Kevin Bierhoff |
| 2012 | Meta-level features in an industrial-strength theorem prover. | J Strother Moore |
| 2012 | A compiler and run-time system for network programming languages. | Christopher Monsanto, Nate Foster, Rob Harrison, David Walker |
| 2012 | Recursive proofs for inductive tree data-structures. | Parthasarathy Madhusudan, Xiaokang Qiu, Andrei Stefanescu |
| 2012 | Canonicity for 2-dimensional type theory. | Daniel R. Licata, Robert Harper |
| 2012 | A rely-guarantee-based simulation for verifying concurrent program transformations. | Hongjin Liang, Xinyu Feng, Ming Fu |
| 2012 | Higher-order functional reactive programming in bounded space. | Neelakantan R. Krishnaswami, Nick Benton, Jan Hoffmann |
| 2012 | Constraints as control. | Ali Sinan Kksal, Viktor Kuncak, Philippe Suter |
| 2012 | Run your research: on the effectiveness of lightweight mechanization. | Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, Robert Bruce Findler |
| 2012 | Compilers must speak properties, not just code: CAL: constraint aggregation language for declarative component-coordination. | Raimund Kirner, Frank Penczek, Alexander V. Shafarenko |
| 2012 | Algebraic foundations for effect-dependent optimisations. | Ohad Kammar, Gordon D. Plotkin |
| 2012 | Underspecified harnesses and interleaved bugs. | Saurabh Joshi, Shuvendu K. Lahiri, Akash Lal |
| 2012 | Information effects. | Roshan P. James, Amr Sabry |
| 2012 | The marriage of bisimulations and Kripke logical relations. | Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis |
| 2012 | Edit lenses. | Martin Hofmann, Benjamin C. Pierce, Daniel Wagner |
| 2012 | Playing in the grey area of proofs. | Krystof Hoder, Laura Kovcs, Andrei Voronkov |
| 2012 | Message of thanks: on the receipt of the 2011 ACM SIGPLAN distinguished achievement award. | Tony Hoare |
| 2012 | Access permission contracts for scripting languages. | Phillip Heidegger, Annette Bieniusa, Peter Thiemann |
| 2012 | Towards a program logic for JavaScript. | Philippa Gardner, Sergio Maffeis, Gareth David Smith |