| 2017 | Gradual refinement types. | Nico Lehmann, ric Tanter |
| 2017 | Fencing off go: liveness and safety for channel-based programming. | Julien Lange, Nicholas Ng, Bernardo Toninho, Nobuko Yoshida |
| 2017 | Beginner's luck: a language for property-based generators. | Leonidas Lampropoulos, Diane Gallois-Wong, Catalin Hritcu, John Hughes, Benjamin C. Pierce, Li-yao Xia |
| 2017 | The geometry of parallelism: classical, probabilistic, and quantum effects. | Ugo Dal Lago, Claudia Faggian, Benot Valiron, Akira Yoshimizu |
| 2017 | Parallel functional arrays. | Ananya Kumar, Guy E. Blelloch, Robert Harper |
| 2017 | A relational model of types-and-effects in higher-order concurrent separation logic. | Morten Krogh-Jespersen, Kasper Svendsen, Lars Birkedal |
| 2017 | Interactive proofs in higher-order concurrent separation logic. | Robbert Krebbers, Amin Timany, Lars Birkedal |
| 2017 | Coming to terms with quantified reasoning. | Laura Kovcs, Simon Robillard, Andrei Voronkov |
| 2017 | LOIS: syntax and semantics. | Eryk Kopczynski, Szymon Torunczyk |
| 2017 | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. | Igor V. Konnov, Marijana Lazic, Helmut Veith, Josef Widder |
| 2017 | On the relationship between higher-order recursion schemes and higher-order fixpoint logic. | Naoki Kobayashi, tienne Lozes, Florian Bruse |
| 2017 | Stream fusion, to completeness. | Oleg Kiselyov, Aggelos Biboudis, Nick Palladinos, Yannis Smaragdakis |
| 2017 | A promising semantics for relaxed-memory concurrency. | Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer |
| 2017 | Sums of uncertainty: refinements go gradual. | Khurram A. Jafery, Jana Dunfield |
| 2017 | The exp-log normal form of types: decomposing extensional equality and representing terms compactly. | Danko Ilik |
| 2017 | Towards automatic resource bound analysis for OCaml. | Jan Hoffmann, Ankush Das, Shu-Chun Weng |
| 2017 | Thread modularity at many levels: a pearl in compositional verification. | Jochen Hoenicke, Rupak Majumdar, Andreas Podelski |
| 2017 | Java generics are turing complete. | Radu Grigore |
| 2017 | A posteriori environment analysis with Pushdown Delta CFA. | Kimball Germane, Matthew Might |
| 2017 | Mixed-size concurrency: ARM, POWER, C/C++11, and SC. | Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, Peter Sewell |
| 2017 | Component-based synthesis for complex APIs. | Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, Thomas W. Reps |
| 2017 | Intersection type calculi of bounded dimension. | Andrej Dudenhefner, Jakob Rehof |
| 2017 | Polymorphism, subtyping, and type inference in MLsub. | Stephen Dolan, Alan Mycroft |
| 2017 | Monadic second-order logic on finite sequences. | Loris D'Antoni, Margus Veanes |
| 2017 | Modules, abstraction, and parametric polymorphism. | Karl Crary |