| 2011 | A kripke logical relation between ML and assembly. Chung-Kil Hur, Derek Dreyer |
| 2011 | A parametric segmentation functor for fully automatic and scalable array content analysis. Patrick Cousot, Radhia Cousot, Francesco Logozzo |
| 2011 | A separation logic for refining concurrent objects. Aaron Joseph Turon, Mitchell Wand |
| 2011 | A shape analysis for optimizing parallel graph programs. Dimitrios Prountzos, Roman Manevich, Keshav Pingali, Kathryn S. McKinley |
| 2011 | A technique for the effective and automatic reuse of classical compiler optimizations on multithreaded code. Pramod G. Joisha, Robert S. Schreiber, Prithviraj Banerjee, Hans-Juergen Boehm, Dhruva R. Chakrabarti |
| 2011 | A typed store-passing translation for general references. François Pottier |
| 2011 | Automating string processing in spreadsheets using input-output examples. Sumit Gulwani |
| 2011 | Bisimulation for quantum processes. Yuan Feng, Runyao Duan, Mingsheng Ying |
| 2011 | Blame for all. Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, Philip Wadler |
| 2011 | Calling context abstraction with shapes. Xavier Rival, Bor-Yuh Evan Chang |
| 2011 | Complexity of pattern-based verification for multithreaded programs. Javier Esparza, Pierre Ganty |
| 2011 | Correct blame for contracts: no more scapegoating. Christos Dimoulas, Robert Bruce Findler, Cormac Flanagan, Matthias Felleisen |
| 2011 | Decidable logics combining heap structures and data. P. Madhusudan, Gennaro Parlato, Xiaokang Qiu |
| 2011 | Delay-bounded scheduling. Michael Emmi, Shaz Qadeer, Zvonimir Rakamaric |
| 2011 | Dynamic inference of static types for ruby. Jong-hoon (David) An, Avik Chaudhuri, Jeffrey S. Foster, Michael Hicks |
| 2011 | Dynamic multirole session types. Pierre-Malo Deniélou, Nobuko Yoshida |
| 2011 | EigenCFA: accelerating flow analysis with GPUs. Tarun Prabhu, Shreyas Ramalingam, Matthew Might, Mary W. Hall |
| 2011 | Expressive modular fine-grained concurrency specification. Bart Jacobs, Frank Piessens |
| 2011 | Formal verification of object layout for c++ multiple inheritance. Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy |
| 2011 | Fresh-register automata. Nikos Tzevelekos |
| 2011 | Generative type abstraction and type-level computation. Stephanie Weirich, Dimitrios Vytiniotis, Simon L. Peyton Jones, Steve Zdancewic |
| 2011 | Geometry of synthesis III: resource management through type inference. Dan R. Ghica, Alex I. Smith |
| 2011 | Laws of order: expensive synchronization in concurrent algorithms cannot be eliminated. Hagit Attiya, Rachid Guerraoui, Danny Hendler, Petr Kuznetsov, Maged M. Michael, Martin T. Vechev |
| 2011 | Learning minimal abstractions. Percy Liang, Omer Tripp, Mayur Naik |
| 2011 | Loop transformations: convexity, pruning and optimization. Louis-Noël Pouchet, Uday Bondhugula, Cédric Bastoul, Albert Cohen, J. Ramanujam, P. Sadayappan, Nicolas Vasilache |
| 2011 | Making prophecies with decision predicates. Byron Cook, Eric Koskinen |
| 2011 | Mathematizing C++ concurrency. Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber |
| 2011 | Modular reasoning for deterministic parallelism. Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson |
| 2011 | Multivariate amortized resource analysis. Jan Hoffmann, Klaus Aehlig, Martin Hofmann |
| 2011 | On interference abstractions. Nishant Sinha, Chao Wang |
| 2011 | Pick your contexts well: understanding object-sensitivity. Yannis Smaragdakis, Martin Bravenboer, Ondrej Lhoták |
| 2011 | Points-to analysis with efficient strong updates. Ondrej Lhoták, Kwok-Chiang Andrew Chung |
| 2011 | Practical affine types. Jesse A. Tov, Riccardo Pucella |
| 2011 | Precise reasoning for programs using containers. Isil Dillig, Thomas Dillig, Alex Aiken |
| 2011 | Predicate abstraction and refinement for verifying multi-threaded programs. Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko |
| 2011 | Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011 Thomas Ball, Mooly Sagiv |
| 2011 | Regular expression containment: coinductive axiomatization and computational interpretation. Fritz Henglein, Lasse Nielsen |
| 2011 | Relaxed-memory concurrency and verified compilation. Jaroslav Sevcík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell |
| 2011 | Resourceable, retargetable, modular instruction selection using a machine-independent, type-based tiling of low-level intermediate code. Norman Ramsey, João Dias |
| 2011 | Robin Milner 1934--2010: verification, languages, and concurrency. Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, Peter Sewell |
| 2011 | Safe nondeterminism in a deterministic-by-default parallel language. Robert L. Bocchino Jr., Stephen Heumann, Nima Honarmand, Sarita V. Adve, Vikram S. Adve, Adam Welc, Tatiana Shpeisman |
| 2011 | Space overhead bounds for dynamic memory management with partial compaction. Anna Bendersky, Erez Petrank |
| 2011 | Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. Martin D. Schwarz, Helmut Seidl, Vesal Vojdani, Peter Lammich, Markus Müller-Olm |
| 2011 | Static analysis of multi-staged programs via unstaging translation. Wontae Choi, Baris Aktemur, Kwangkeun Yi, Makoto Tatsuta |
| 2011 | Step-indexed kripke models over recursive worlds. Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Støvring, Jacob Thamsborg, Hongseok Yang |
| 2011 | Streaming transducers for algorithmic verification of single-pass list-processing programs. Rajeev Alur, Pavol Cerný |
| 2011 | Symmetric lenses. Martin Hofmann, Benjamin C. Pierce, Daniel Wagner |
| 2011 | The design of kodu: a tiny visual programming language for children on the Xbox 360. Matthew MacLaurin |
| 2011 | The essence of compiling with traces. Shu-Yu Guo, Jens Palsberg |
| 2011 | The tree width of auxiliary storage. P. Madhusudan, Gennaro Parlato |
| 2011 | Vector addition system reachability problem: a short self-contained proof. Jérôme Leroux |
| 2011 | Verified squared: does critical software deserve verified tools? Xavier Leroy |
| 2011 | Verifying higher-order functional programs with pattern-matching algebraic data types. C.-H. Luke Ong, Steven J. Ramsay |