| 2016 | 'Cause I'm strong enough: reasoning about consistency choices in distributed systems. Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, Marc Shapiro |
| 2016 | A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. Jean Pichon-Pharabod, Peter Sewell |
| 2016 | A program logic for concurrent objects under fair scheduling. Hongjin Liang, Xinyu Feng |
| 2016 | A theory of effects and resources: adjunction models and polarised calculi. Pierre-Louis Curien, Marcelo P. Fiore, Guillaume Munch-Maccagnoni |
| 2016 | Abstracting gradual typing. Ronald Garcia, Alison M. Clark, Éric Tanter |
| 2016 | Abstraction refinement guided by a learnt probabilistic model. Radu Grigore, Hongseok Yang |
| 2016 | Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, Rouzbeh Hasheminezhad |
| 2016 | Algorithms for algebraic path properties in concurrent systems of constant treewidth components. Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis |
| 2016 | Automatic patch generation by learning correct code. Fan Long, Martin C. Rinard |
| 2016 | Binding as sets of scopes. Matthew Flatt |
| 2016 | Breaking through the normalization barrier: a self-interpreter for f-omega. Matt Brown, Jens Palsberg |
| 2016 | Casper: an efficient approach to call trace collection. Rongxin Wu, Xiao Xiao, Shing-Chi Cheung, Hongyu Zhang, Charles Zhang |
| 2016 | Chapar: certified causally consistent distributed key-value stores. Mohsen Lesani, Christian J. Bell, Adam Chlipala |
| 2016 | Combining static analysis with probabilistic models to enable market-scale Android inter-component analysis. Damien Octeau, Somesh Jha, Matthew L. Dering, Patrick D. McDaniel, Alexandre Bartel, Li Li, Jacques Klein, Yves Le Traon |
| 2016 | Confluences in programming languages research (keynote). David Walker |
| 2016 | Decidability of inferring inductive invariants. Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv |
| 2016 | Dependent types and multi-monadic effects in F. Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, Santiago Zanella-Béguelin |
| 2016 | Effects as sessions, sessions as effects. Dominic A. Orchard, Nobuko Yoshida |
| 2016 | Environmental bisimulations for probabilistic higher-order languages. Davide Sangiorgi, Valeria Vignudelli |
| 2016 | Estimating types in binaries using predictive modeling. Omer Katz, Ran El-Yaniv, Eran Yahav |
| 2016 | Example-directed synthesis: a type-theoretic interpretation. Jonathan Frankle, Peter-Michael Osera, David Walker, Steve Zdancewic |
| 2016 | Fabular: regression formulas as probabilistic programming. Johannes Borgström, Andrew D. Gordon, Long Ouyang, Claudio V. Russo, Adam Scibior, Marcin Szymczak |
| 2016 | From MinX to MinC: semantics-driven decompilation of recursive datatypes. Edward Robbins, Andy King, Tom Schrijvers |
| 2016 | Fully-abstract compilation by approximate back-translation. Dominique Devriese, Marco Patrignani, Frank Piessens |
| 2016 | Is sound gradual typing dead? Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, Matthias Felleisen |
| 2016 | Kleenex: compiling nondeterministic transducers to deterministic streaming transducers. Niels Bjørn Bugge Grathwohl, Fritz Henglein, Ulrik Terp Rasmussen, Kristoffer Aalund Søholm, Sebastian Paaske Tørholm |
| 2016 | Lattice-theoretic progress measures and coalgebraic model checking. Ichiro Hasuo, Shunsuke Shimizu, Corina Cîrstea |
| 2016 | Learning invariants using decision trees and implication counterexamples. Pranav Garg, Daniel Neider, P. Madhusudan, Dan Roth |
| 2016 | Learning programs from noisy data. Veselin Raychev, Pavol Bielik, Martin T. Vechev, Andreas Krause |
| 2016 | Lightweight verification of separate compilation. Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis |
| 2016 | Maximal specification synthesis. Aws Albarghouthi, Isil Dillig, Arie Gurfinkel |
| 2016 | Memoryful geometry of interaction II: recursion and adequacy. Koko Muroya, Naohiko Hoshino, Ichiro Hasuo |
| 2016 | Model checking for symbolic-heap separation logic with inductive predicates. James Brotherston, Nikos Gorogiannis, Max I. Kanovich, Reuben Rowe |
| 2016 | Modelling the ARMv8 architecture, operationally: concurrency and ISA. Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, Peter Sewell |
| 2016 | Monitors and blame assignment for higher-order session types. Limin Jia, Hannah Gommerstadt, Frank Pfenning |
| 2016 | Newtonian program analysis via tensor product. Thomas W. Reps, Emma Turetsky, Prathmesh Prabhu |
| 2016 | Optimizing synthesis with metasketches. James Bornholt, Emina Torlak, Dan Grossman, Luis Ceze |
| 2016 | Overhauling SC atomics in C11 and OpenCL. Mark Batty, Alastair F. Donaldson, John Wickerson |
| 2016 | PSync: a partially synchronous language for fault-tolerant distributed algorithms. Cezara Dragoi, Thomas A. Henzinger, Damien Zufferey |
| 2016 | PolyCheck: dynamic verification of iteration space transformations on affine programs. Wenlei Bao, Sriram Krishnamoorthy, Louis-Noël Pouchet, Fabrice Rastello, P. Sadayappan |
| 2016 | Principal type inference for GADTs. Sheng Chen, Martin Erwig |
| 2016 | Printing floating-point numbers: a faster, always correct method. Marc Andrysco, Ranjit Jhala, Sorin Lerner |
| 2016 | Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016 Rastislav Bodík, Rupak Majumdar |
| 2016 | Programming the world of uncertain things (keynote). Kathryn S. McKinley |
| 2016 | Pushdown control-flow analysis for free. Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, David Van Horn |
| 2016 | Query-guided maximum satisfiability. Xin Zhang, Ravi Mangal, Aditya V. Nori, Mayur Naik |
| 2016 | Reducing crash recoverability to reachability. Eric Koskinen, Junfeng Yang |
| 2016 | SMO: an integrated approach to intra-array and inter-array storage optimization. Somashekaracharya G. Bhaskaracharya, Uday Bondhugula, Albert Cohen |
| 2016 | Scaling network verification using symmetry and surgery. Gordon D. Plotkin, Nikolaj S. Bjørner, Nuno P. Lopes, Andrey Rybalchenko, George Varghese |
| 2016 | Sound type-dependent syntactic language extension. Florian Lorenzen, Sebastian Erdweg |
| 2016 | String solving with word equations and transducers: towards a logic for analysing mutation XSS. Anthony Widjaja Lin, Pablo Barceló |
| 2016 | Symbolic abstract data type inference. Michael Emmi, Constantin Enea |
| 2016 | Symbolic computation of differential equivalences. Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin |
| 2016 | Synthesis of reactive controllers for hybrid systems (keynote). Richard M. Murray |
| 2016 | System f-omega with equirecursive types for datatype-generic programming. Yufei Cai, Paolo G. Giarrusso, Klaus Ostermann |
| 2016 | Taming release-acquire consistency. Ori Lahav, Nick Giannarakis, Viktor Vafeiadis |
| 2016 | Temporal verification of higher-order functional programs. Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno |
| 2016 | The complexity of interaction. Stéphane Gimenez, Georg Moser |
| 2016 | The gradualizer: a methodology and algorithm for generating gradual type systems. Matteo Cimini, Jeremy G. Siek |
| 2016 | The hardness of data packing. Rahman Lavaee |
| 2016 | Transforming spreadsheet data types using examples. Rishabh Singh, Sumit Gulwani |
| 2016 | Type theory in type theory using quotient inductive types. Thorsten Altenkirch, Ambrus Kaposi |
| 2016 | Unboundedness and downward closures of higher-order pushdown automata. Matthew Hague, Jonathan Kochems, C.-H. Luke Ong |