| 2016 | 'Cause I'm strong enough: reasoning about consistency choices in distributed systems. | Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, Marc Shapiro |
| 2016 | The complexity of interaction. | Stphane Gimenez, Georg Moser |
| 2016 | Pushdown control-flow analysis for free. | Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, David Van Horn |
| 2016 | Abstracting gradual typing. | Ronald Garcia, Alison M. Clark, ric Tanter |
| 2016 | Example-directed synthesis: a type-theoretic interpretation. | Jonathan Frankle, Peter-Michael Osera, David Walker, Steve Zdancewic |
| 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 | Binding as sets of scopes. | Matthew Flatt |
| 2016 | Symbolic abstract data type inference. | Michael Emmi, Constantin Enea |
| 2016 | PSync: a partially synchronous language for fault-tolerant distributed algorithms. | Cezara Dragoi, Thomas A. Henzinger, Damien Zufferey |
| 2016 | Fully-abstract compilation by approximate back-translation. | Dominique Devriese, Marco Patrignani, Frank Piessens |
| 2016 | A theory of effects and resources: adjunction models and polarised calculi. | Pierre-Louis Curien, Marcelo P. Fiore, Guillaume Munch-Maccagnoni |
| 2016 | The gradualizer: a methodology and algorithm for generating gradual type systems. | Matteo Cimini, Jeremy G. Siek |
| 2016 | Algorithms for algebraic path properties in concurrent systems of constant treewidth components. | Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis |
| 2016 | Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. | Krishnendu Chatterjee, Hongfei Fu, Petr Novotn, Rouzbeh Hasheminezhad |
| 2016 | Symbolic computation of differential equivalences. | Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin |
| 2016 | System f-omega with equirecursive types for datatype-generic programming. | Yufei Cai, Paolo G. Giarrusso, Klaus Ostermann |
| 2016 | Breaking through the normalization barrier: a self-interpreter for f-omega. | Matt Brown, Jens Palsberg |
| 2016 | Model checking for symbolic-heap separation logic with inductive predicates. | James Brotherston, Nikos Gorogiannis, Max I. Kanovich, Reuben Rowe |
| 2016 | Optimizing synthesis with metasketches. | James Bornholt, Emina Torlak, Dan Grossman, Luis Ceze |
| 2016 | Fabular: regression formulas as probabilistic programming. | Johannes Borgstrm, Andrew D. Gordon, Long Ouyang, Claudio V. Russo, Adam Scibior, Marcin Szymczak |
| 2016 | SMO: an integrated approach to intra-array and inter-array storage optimization. | Somashekaracharya G. Bhaskaracharya, Uday Bondhugula, Albert Cohen |
| 2016 | Overhauling SC atomics in C11 and OpenCL. | Mark Batty, Alastair F. Donaldson, John Wickerson |
| 2016 | PolyCheck: dynamic verification of iteration space transformations on affine programs. | Wenlei Bao, Sriram Krishnamoorthy, Louis-Nol Pouchet, Fabrice Rastello, P. Sadayappan |
| 2016 | Printing floating-point numbers: a faster, always correct method. | Marc Andrysco, Ranjit Jhala, Sorin Lerner |
| 2016 | Type theory in type theory using quotient inductive types. | Thorsten Altenkirch, Ambrus Kaposi |