POPL 2015

55 papers

1. A Calculus for Relaxed Memory · Karl Crary, Michael J. Sullivan
2. A Coalgebraic Decision Procedure for NetKAT · Nate Foster, Dexter Kozen, Mae Milano, Alexandra Silva, Laure Thompson
3. A Formally-Verified C Static Analyzer · Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie
4. A Meta Lambda Calculus with Cross-Level Computation · Kazunori Tobisawa
5. A Scalable, Correct Time-Stamped Stack · Mike Dodds, Andreas Haas, Christoph M. Kirsch
6. Abstract Symbolic Automata: Mixed syntactic/semantic similarity analysis of executables · Mila Dalla Preda, Roberto Giacobazzi, Arun Lakhotia, Isabella Mastroeni
7. Algebraic Effects, Linearity, and Quantum Programming Languages · Sam Staton
8. Analyzing Program Analyses · Roberto Giacobazzi, Francesco Logozzo, Francesco Ranzato
9. Automating Repetitive Tasks for the Masses · Sumit Gulwani
10. Coding by Everyone, Every Day · Peter Lee
11. Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it · Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli
12. Compositional CompCert · Gordon Stewart, Lennart Beringer, Santiago Cuéllar, Andrew W. Appel
13. Conjugate Hylomorphisms - Or: The Mother of All Structured Recursion Schemes · Ralf Hinze, Nicolas Wu, Jeremy Gibbons
14. DReX: A Declarative Language for Efficiently Evaluating Regular String Transformations · Rajeev Alur, Loris D'Antoni, Mukund Raghothaman
15. Data-Parallel String-Manipulating Programs · Margus Veanes, Todd Mytkowicz, David Molnar, Benjamin Livshits
16. Databases and Programming: Two Subjects Divided by a Common Language? · Peter Buneman
17. Decentralizing SDN Policies · Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham
18. Deep Specifications and Certified Abstraction Layers · Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng + 2 more
19. Dependent Information Flow Types · Luísa Lourenço, Luís Caires
20. Differential Privacy: Now it's Getting Personal · Hamid Ebadi, David Sands, Gerardo Schneider
21. Equations, Contractions, and Unique Solutions · Davide Sangiorgi
22. Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth · Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Andreas Pavlogiannis, Prateesh Goyal
23. Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant · Benjamin Delaware, Clément Pit-Claudel, Jason Gross, Adam Chlipala
24. From Communicating Machines to Graphical Choreographies · Julien Lange, Emilio Tuosto, Nobuko Yoshida
25. From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification · Adam Chlipala
26. Full Abstraction for Signal Flow Graphs · Filippo Bonchi, Pawel Sobocinski, Fabio Zanasi
27. Functors are Type Refinement Systems · Paul-André Melliès, Noam Zeilberger
28. Higher Inductive Types as Homotopy-Initial Algebras · Kristina Sojakova
29. Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy · Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub
30. Integrating Linear and Dependent Types · Neelakantan R. Krishnaswami, Cécilia Pradic, Nick Benton
31. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning · Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal + 1 more
32. K-Java: A Complete Semantics of Java · Denis Bogdanas, Grigore Rosu
33. Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems · Fei He, Xiaowei Gao, Bow-Yaw Wang, Lijun Zhang
34. Manifest Contracts for Datatypes · Taro Sekiyama, Yuki Nishida, Atsushi Igarashi
35. On Characterizing the Data Access Complexity of Programs · Venmugil Elango, Fabrice Rastello, Louis-Noël Pouchet, J. Ramanujam, P. Sadayappan
36. Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type Reconstruction · Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Pietro Abate
37. Predicting Program Properties from "Big Code" · Veselin Raychev, Martin T. Vechev, Andreas Krause
38. Principal Type Schemes for Gradual Programs · Ronald Garcia, Matteo Cimini
39. Probabilistic Termination: Soundness, Completeness, and Compositionality · Luis María Ferrer Fioriti, Holger Hermanns
40. Program Boosting: Program Synthesis via Crowd-Sourcing · Robert A. Cochran, Loris D'Antoni, Benjamin Livshits, David Molnar, Margus Veanes
41. Programming up to Congruence · Vilhelm Sjöberg, Stephanie Weirich
42. Proof Spaces for Unbounded Parallelism · Azadeh Farzan, Zachary Kincaid, Andreas Podelski
43. Quantitative Interprocedural Analysis · Krishnendu Chatterjee, Andreas Pavlogiannis, Yaron Velner
44. Runtime Enforcement of Security Policies on Black Box Reactive Programs · Minh Ngo, Fabio Massacci, Dimiter Milushev, Frank Piessens
45. Safe & Efficient Gradual Typing for TypeScript · Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin M. Bierman, Panagiotis Vekris
46. Self-Representation in Girard's System U · Matt Brown, Jens Palsberg
47. Sound Modular Verification of C Code Executing in an Unverified Context · Pieter Agten, Bart Jacobs, Frank Piessens
48. Space-Efficient Manifest Contracts · Michael Greenberg
49. Specification Inference Using Context-Free Language Reachability · Osbert Bastani, Saswat Anand, Alex Aiken
50. Succinct Representation of Concurrent Trace Sets · Ashutosh Gupta, Thomas A. Henzinger, Arjun Radhakrishna, Roopsha Samanta, Thorsten Tarrach
51. Summary-Based Context-Sensitive Data-Dependence Analysis in Presence of Callbacks · Hao Tang, Xiaoyin Wang, Lingming Zhang, Bing Xie, Lu Zhang, Hong Mei
52. Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests · Damien Pous
53. Towards the Essence of Hygiene · Michael D. Adams
54. Tractable Refinement Checking for Concurrent Objects · Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
55. Ur/Web: A Simple Model for Programming the Web · Adam Chlipala