| 2012 | A compiler and run-time system for network programming languages. Christopher Monsanto, Nate Foster, Rob Harrison, David Walker |
| 2012 | A language for automatically enforcing privacy policies. Jean Yang, Kuat Yessenov, Armando Solar-Lezama |
| 2012 | A mechanized semantics for C++ object construction and destruction, with applications to resource management. Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy |
| 2012 | A rely-guarantee-based simulation for verifying concurrent program transformations. Hongjin Liang, Xinyu Feng, Ming Fu |
| 2012 | A type system for borrowing permissions. Karl Naden, Robert Bocchino, Jonathan Aldrich, Kevin Bierhoff |
| 2012 | A type theory for probability density functions. Sooraj Bhat, Ashish Agarwal, Richard W. Vuduc, Alexander G. Gray |
| 2012 | A unified approach to fully lazy sharing. Thibaut Balabonski |
| 2012 | Abstractions from tests. Mayur Naik, Hongseok Yang, Ghila Castelnuovo, Mooly Sagiv |
| 2012 | Access permission contracts for scripting languages. Phillip Heidegger, Annette Bieniusa, Peter Thiemann |
| 2012 | Algebraic foundations for effect-dependent optimisations. Ohad Kammar, Gordon D. Plotkin |
| 2012 | An abstract interpretation framework for termination. Patrick Cousot, Radhia Cousot |
| 2012 | An executable formal semantics of C with applications. Chucky Ellison, Grigore Rosu |
| 2012 | Analysis of recursively parallel programs. Ahmed Bouajjani, Michael Emmi |
| 2012 | Canonicity for 2-dimensional type theory. Daniel R. Licata, Robert Harper |
| 2012 | Clarifying and compiling C/C++ concurrency: from C++11 to POWER. Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, Peter Sewell |
| 2012 | Constraints as control. Ali Sinan Köksal, Viktor Kuncak, Philippe Suter |
| 2012 | Deciding choreography realizability. Samik Basu, Tevfik Bultan, Meriem Ouederni |
| 2012 | Defining code-injection attacks. Donald Ray, Jay Ligatti |
| 2012 | Edit lenses. Martin Hofmann, Benjamin C. Pierce, Daniel Wagner |
| 2012 | Formalizing the LLVM intermediate representation for verified program transformations. Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic |
| 2012 | Freefinement. Stephan van Staden, Cristiano Calcagno, Bertrand Meyer |
| 2012 | Higher-order functional reactive programming in bounded space. Neelakantan R. Krishnaswami, Nick Benton, Jan Hoffmann |
| 2012 | Information effects. Roshan P. James, Amr Sabry |
| 2012 | Message of thanks: on the receipt of the 2011 ACM SIGPLAN distinguished achievement award. Tony Hoare |
| 2012 | Meta-level features in an industrial-strength theorem prover. J Strother Moore |
| 2012 | Multiple facets for dynamic information flow. Thomas H. Austin, Cormac Flanagan |
| 2012 | Nested refinements: a logic for duck typing. Ravi Chugh, Patrick Maxim Rondon, Ranjit Jhala |
| 2012 | On the power of coercion abstraction. Julien Cretin, Didier Rémy |
| 2012 | Playing in the grey area of proofs. Krystof Hoder, Laura Kovács, Andrei Voronkov |
| 2012 | Presentation of the SIGPLAN distinguished achievement award to Sir Charles Antony Richard Hoare, FRS, FREng, FBCS; and interview. Andrew P. Black, Peter W. O'Hearn |
| 2012 | Probabilistic relational reasoning for differential privacy. Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella-Béguelin |
| 2012 | Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012 John Field, Michael Hicks |
| 2012 | Programming languages for programmable networks. Jennifer Rexford |
| 2012 | Programming with binders and indexed data-types. Andrew Cave, Brigitte Pientka |
| 2012 | Randomized accuracy-aware program transformations for efficient approximate computations. Zeyuan Allen Zhu, Sasa Misailovic, Jonathan A. Kelner, Martin C. Rinard |
| 2012 | Recursive proofs for inductive tree data-structures. Parthasarathy Madhusudan, Xiaokang Qiu, Andrei Stefanescu |
| 2012 | Resource-sensitive synchronization inference by abduction. Matko Botincan, Mike Dodds, Suresh Jagannathan |
| 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 | Self-certification: bootstrapping certified typecheckers in F* with Coq. Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen |
| 2012 | Sound predictive race detection in polynomial time. Yannis Smaragdakis, Jacob Evans, Caitlin Sadowski, Jaeheon Yi, Cormac Flanagan |
| 2012 | Static and user-extensible proof checking. Antonis Stampoulis, Zhong Shao |
| 2012 | Symbolic finite state transducers: algorithms and applications. Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, Nikolaj S. Bjørner |
| 2012 | Syntactic control of interference for separation logic. Uday S. Reddy, John C. Reynolds |
| 2012 | The ins and outs of gradual type inference. Aseem Rastogi, Avik Chaudhuri, Basil Hosmer |
| 2012 | The marriage of bisimulations and Kripke logical relations. Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis |
| 2012 | Towards a program logic for JavaScript. Philippa Gardner, Sergio Maffeis, Gareth David Smith |
| 2012 | Towards nominal computation. Mikolaj Bojanczyk, Laurent Braud, Bartek Klin, Slawomir Lasota |
| 2012 | Underspecified harnesses and interleaved bugs. Saurabh Joshi, Shuvendu K. Lahiri, Akash Lal |
| 2012 | Verification of parameterized concurrent programs by modular reasoning about data and control. Azadeh Farzan, Zachary Kincaid |