POPL 2012

48 papers

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