Abstract is missing.
- Presentation of the SIGPLAN distinguished achievement award to Sir Charles Antony Richard Hoare, FRS, FREng, FBCS; and interviewAndrew P. Black, Peter W. O'Hearn. 1-2 [doi]
- Message of thanks: on the receipt of the 2011 ACM SIGPLAN distinguished achievement awardTony Hoare. 3-6 [doi]
- FreefinementStephan van Staden, Cristiano Calcagno, Bertrand Meyer. 7-18 [doi]
- Underspecified harnesses and interleaved bugsSaurabh Joshi 0001, Shuvendu K. Lahiri, Akash Lal. 19-30 [doi]
- Towards a program logic for JavaScriptPhilippa Gardner, Sergio Maffeis, Gareth David Smith. 31-44 [doi]
- Higher-order functional reactive programming in bounded spaceNeelakantan R. Krishnaswami, Nick Benton, Jan Hoffmann 0002. 45-58 [doi]
- The marriage of bisimulations and Kripke logical relationsChung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis. 59-72 [doi]
- Information effectsRoshan P. James, Amr Sabry. 73-84 [doi]
- A language for automatically enforcing privacy policiesJean Yang, Kuat Yessenov, Armando Solar-Lezama. 85-96 [doi]
- Probabilistic relational reasoning for differential privacyGilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella Béguelin. 97-110 [doi]
- Access permission contracts for scripting languagesPhillip Heidegger, Annette Bieniusa, Peter Thiemann. 111-122 [doi]
- Recursive proofs for inductive tree data-structuresParthasarathy Madhusudan, Xiaokang Qiu, Andrei Stefanescu. 123-136 [doi]
- Symbolic finite state transducers: algorithms and applicationsMargus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, Nikolaj Bjørner. 137-150 [doi]
- Constraints as controlAli Sinan Köksal, Viktor Kuncak, Philippe Suter. 151-164 [doi]
- Multiple facets for dynamic information flowThomas H. Austin, Cormac Flanagan. 165-178 [doi]
- Defining code-injection attacksDonald Ray, Jay Ligatti. 179-190 [doi]
- Deciding choreography realizabilitySamik Basu, Tevfik Bultan, Meriem Ouederni. 191-202 [doi]
- Analysis of recursively parallel programsAhmed Bouajjani, Michael Emmi. 203-214 [doi]
- Programming languages for programmable networksJennifer Rexford. 215-216 [doi]
- A compiler and run-time system for network programming languagesChristopher Monsanto, Nate Foster, Rob Harrison, David Walker. 217-230 [doi]
- Nested refinements: a logic for duck typingRavi Chugh, Patrick Maxim Rondon, Ranjit Jhala. 231-244 [doi]
- An abstract interpretation framework for terminationPatrick Cousot, Radhia Cousot. 245-258 [doi]
- Playing in the grey area of proofsKrystof Hoder, Laura Kovács, Andrei Voronkov. 259-272 [doi]
- Static and user-extensible proof checkingAntonis Stampoulis, Zhong Shao. 273-284 [doi]
- Run your research: on the effectiveness of lightweight mechanizationCasey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, Robby Findler. 285-296 [doi]
- Verification of parameterized concurrent programs by modular reasoning about data and controlAzadeh Farzan, Zachary Kincaid. 297-308 [doi]
- Resource-sensitive synchronization inference by abductionMatko Botincan, Mike Dodds, Suresh Jagannathan. 309-322 [doi]
- Syntactic control of interference for separation logicUday S. Reddy, John C. Reynolds. 323-336 [doi]
- Canonicity for 2-dimensional type theoryDaniel R. Licata, Robert Harper. 337-348 [doi]
- Algebraic foundations for effect-dependent optimisationsOhad Kammar, Gordon D. Plotkin. 349-360 [doi]
- On the power of coercion abstractionJulien Cretin, Didier Rémy. 361-372 [doi]
- Abstractions from testsMayur Naik, Hongseok Yang, Ghila Castelnuovo, Mooly Sagiv. 373-386 [doi]
- Sound predictive race detection in polynomial timeYannis Smaragdakis, Jacob Evans, Caitlin Sadowski, Jaeheon Yi, Cormac Flanagan. 387-400 [doi]
- Towards nominal computationMikolaj Bojanczyk, Laurent Braud, Bartek Klin, Slawomir Lasota. 401-412 [doi]
- Programming with binders and indexed data-typesAndrew Cave, Brigitte Pientka. 413-424 [doi]
- Meta-level features in an industrial-strength theorem proverJ. Strother Moore. 425-426 [doi]
- Formalizing the LLVM intermediate representation for verified program transformationsJianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic. 427-440 [doi]
- Randomized accuracy-aware program transformations for efficient approximate computationsZeyuan Allen Zhu, Sasa Misailovic, Jonathan A. Kelner, Martin C. Rinard. 441-454 [doi]
- A rely-guarantee-based simulation for verifying concurrent program transformationsHongjin Liang, Xinyu Feng, Ming Fu. 455-468 [doi]
- A unified approach to fully lazy sharingThibaut Balabonski. 469-480 [doi]
- The ins and outs of gradual type inferenceAseem Rastogi, Avik Chaudhuri, Basil Hosmer. 481-494 [doi]
- Edit lensesMartin Hofmann, Benjamin C. Pierce, Daniel Wagner. 495-508 [doi]
- Clarifying and compiling C/C++ concurrency: from C++11 to POWERMark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, Peter Sewell. 509-520 [doi]
- A mechanized semantics for C++ object construction and destruction, with applications to resource managementTahina Ramananandro, Gabriel Dos Reis, Xavier Leroy. 521-532 [doi]
- An executable formal semantics of C with applicationsChucky Ellison, Grigore Rosu. 533-544 [doi]
- A type theory for probability density functionsSooraj Bhat, Ashish Agarwal, Richard W. Vuduc, Alexander G. Gray. 545-556 [doi]
- A type system for borrowing permissionsKarl Naden, Robert Bocchino, Jonathan Aldrich, Kevin Bierhoff. 557-570 [doi]
- Self-certification: bootstrapping certified typecheckers in F* with CoqPierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen. 571-584 [doi]