| 2017 | A posteriori environment analysis with Pushdown Delta CFA. Kimball Germane, Matthew Might |
| 2017 | A program optimization for automatic database result caching. Ziv Scully, Adam Chlipala |
| 2017 | A promising semantics for relaxed-memory concurrency. Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer |
| 2017 | A relational model of types-and-effects in higher-order concurrent separation logic. Morten Krogh-Jespersen, Kasper Svendsen, Lars Birkedal |
| 2017 | A semantic account of metric preservation. Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, Ikram Cherigui |
| 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 | Analyzing divergence in bisimulation semantics. Xinxin Liu, Tingting Yu, Wenhui Zhang |
| 2017 | Automatically comparing memory consistency models. John Wickerson, Mark Batty, Tyler Sorensen, George A. Constantinides |
| 2017 | Automatically generating the dynamic semantics of gradually typed languages. Matteo Cimini, Jeremy G. Siek |
| 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 | Big types in little runtime: open-world soundness and collaborative blame for gradual type systems. Michael M. Vitousek, Cameron Swords, Jeremy G. Siek |
| 2017 | Cantor meets scott: semantic foundations for probabilistic networks. Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, Alexandra Silva |
| 2017 | Coming to terms with quantified reasoning. Laura Kovács, Simon Robillard, Andrei Voronkov |
| 2017 | Complexity verification using guided theorem enumeration. Akhilesh Srikanth, Burak Sahin, William R. Harris |
| 2017 | Component-based synthesis for complex APIs. Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, Thomas W. Reps |
| 2017 | Computational higher-dimensional type theory. Carlo Angiuli, Robert Harper, Todd Wilson |
| 2017 | Context-sensitive data-dependence analysis via linear conjunctive language reachability. Qirun Zhang, Zhendong Su |
| 2017 | Contextual isomorphisms. Paul Blain Levy |
| 2017 | Contract-based resource verification for higher-order functions with memoization. Ravichandhran Madhavan, Sumith Kulal, Viktor Kuncak |
| 2017 | Coupling proofs are probabilistic product programs. Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub |
| 2017 | Deciding equivalence with sums and the empty type. Gabriel Scherer |
| 2017 | Dijkstra monads for free. Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy |
| 2017 | Do be do be do. Sam Lindley, Conor McBride, Craig McLaughlin |
| 2017 | Dynamic race detection for C++11. Christopher Lidbury, Alastair F. Donaldson |
| 2017 | Exact Bayesian inference by symbolic disintegration. Chung-chieh Shan, Norman Ramsey |
| 2017 | Fast polyhedra abstract domain. Gagandeep Singh, Markus Püschel, Martin T. Vechev |
| 2017 | Fencing off go: liveness and safety for channel-based programming. Julien Lange, Nicholas Ng, Bernardo Toninho, Nobuko Yoshida |
| 2017 | Genesis: synthesizing forwarding tables in multi-tenant networks. Kausik Subramanian, Loris D'Antoni, Aditya Akella |
| 2017 | Gradual refinement types. Nico Lehmann, Éric Tanter |
| 2017 | Hazelnut: a bidirectionally typed structure editor calculus. Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, Matthew A. Hammer |
| 2017 | Hypercollecting semantics and its application to static analysis of information flow. Mounir Assaf, David A. Naumann, Julien Signoles, Eric Totel, Frédéric Tronel |
| 2017 | Interactive proofs in higher-order concurrent separation logic. Robbert Krebbers, Amin Timany, Lars Birkedal |
| 2017 | Intersection type calculi of bounded dimension. Andrej Dudenhefner, Jakob Rehof |
| 2017 | Invariants of quantum programs: characterisations and generation. Mingsheng Ying, Shenggang Ying, Xiaodi Wu |
| 2017 | Java generics are turing complete. Radu Grigore |
| 2017 | LMS-Verify: abstraction without regret for verified systems programming. Nada Amin, Tiark Rompf |
| 2017 | LOIS: syntax and semantics. Eryk Kopczynski, Szymon Torunczyk |
| 2017 | Learning nominal automata. Joshua Moerman, Matteo Sammartino, Alexandra Silva, Bartek Klin, Michal Szynwelski |
| 2017 | LightDP: towards automating differential privacy proofs. Danfeng Zhang, Daniel Kifer |
| 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 | Modules, abstraction, and parametric polymorphism. Karl Crary |
| 2017 | Monadic second-order logic on finite sequences. Loris D'Antoni, Margus Veanes |
| 2017 | Ogre and Pythia: an invariance proof method for weak consistency models. Jade Alglave, Patrick Cousot |
| 2017 | On the relationship between higher-order recursion schemes and higher-order fixpoint logic. Naoki Kobayashi, Étienne Lozes, Florian Bruse |
| 2017 | On verifying causal consistency. Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, Jad Hamza |
| 2017 | Parallel functional arrays. Ananya Kumar, Guy E. Blelloch, Robert Harper |
| 2017 | Polymorphism, subtyping, and type inference in MLsub. Stephen Dolan, Alan Mycroft |
| 2017 | Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 Giuseppe Castagna, Andrew D. Gordon |
| 2017 | QWIRE: a core language for quantum circuits. Jennifer Paykin, Robert Rand, Steve Zdancewic |
| 2017 | Relational cost analysis. Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann |
| 2017 | Rigorous floating-point mixed-precision tuning. Wei-Fan Chiang, Mark Baranowski, Ian Briggs, Alexey Solovyev, Ganesh Gopalakrishnan, Zvonimir Rakamaric |
| 2017 | Rust: from POPL to practice (keynote). Aaron Turon |
| 2017 | Semantic-directed clumping of disjunctive abstract states. Huisong Li, Francois Berenger, Bor-Yuh Evan Chang, Xavier Rival |
| 2017 | Serializability for eventual consistency: criterion, analysis, and applications. Lucas Brutschy, Dimitar Dimitrov, Peter Müller, Martin T. Vechev |
| 2017 | Stateful manifest contracts. Taro Sekiyama, Atsushi Igarashi |
| 2017 | Stochastic invariants for probabilistic termination. Krishnendu Chatterjee, Petr Novotný, Dorde Zikelic |
| 2017 | Stream fusion, to completeness. Oleg Kiselyov, Aggelos Biboudis, Nick Palladinos, Yannis Smaragdakis |
| 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 | The geometry of parallelism: classical, probabilistic, and quantum effects. Ugo Dal Lago, Claudia Faggian, Benoît Valiron, Akira Yoshimizu |
| 2017 | The influence of dependent types (keynote). Stephanie Weirich |
| 2017 | Thread modularity at many levels: a pearl in compositional verification. Jochen Hoenicke, Rupak Majumdar, Andreas Podelski |
| 2017 | Towards automatic resource bound analysis for OCaml. Jan Hoffmann, Ankush Das, Shu-Chun Weng |
| 2017 | Type directed compilation of row-typed algebraic effects. Daan Leijen |
| 2017 | Type soundness proofs with definitional interpreters. Nada Amin, Tiark Rompf |
| 2017 | Type systems as macros. Stephen Chang, Alex Knauth, Ben Greenman |
| 2017 | Typed self-evaluation via intensional type functions. Matt Brown, Jens Palsberg |