| 2017 | Context-sensitive data-dependence analysis via linear conjunctive language reachability. | Qirun Zhang, Zhendong Su |
| 2017 | LightDP: towards automating differential privacy proofs. | Danfeng Zhang, Daniel Kifer |
| 2017 | Invariants of quantum programs: characterisations and generation. | Mingsheng Ying, Shenggang Ying, Xiaodi Wu |
| 2017 | Automatically comparing memory consistency models. | John Wickerson, Mark Batty, Tyler Sorensen, George A. Constantinides |
| 2017 | The influence of dependent types (keynote). | Stephanie Weirich |
| 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 | Rust: from POPL to practice (keynote). | Aaron Turon |
| 2017 | Genesis: synthesizing forwarding tables in multi-tenant networks. | Kausik Subramanian, Loris D'Antoni, Aditya Akella |
| 2017 | Complexity verification using guided theorem enumeration. | Akhilesh Srikanth, Burak Sahin, William R. Harris |
| 2017 | Cantor meets scott: semantic foundations for probabilistic networks. | Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, Alexandra Silva |
| 2017 | Fast polyhedra abstract domain. | Gagandeep Singh, Markus Pschel, Martin T. Vechev |
| 2017 | Exact Bayesian inference by symbolic disintegration. | Chung-chieh Shan, Norman Ramsey |
| 2017 | Stateful manifest contracts. | Taro Sekiyama, Atsushi Igarashi |
| 2017 | A program optimization for automatic database result caching. | Ziv Scully, Adam Chlipala |
| 2017 | Deciding equivalence with sums and the empty type. | Gabriel Scherer |
| 2017 | QWIRE: a core language for quantum circuits. | Jennifer Paykin, Robert Rand, Steve Zdancewic |
| 2017 | Hazelnut: a bidirectionally typed structure editor calculus. | Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, Matthew A. Hammer |
| 2017 | Learning nominal automata. | Joshua Moerman, Matteo Sammartino, Alexandra Silva, Bartek Klin, Michal Szynwelski |
| 2017 | Contract-based resource verification for higher-order functions with memoization. | Ravichandhran Madhavan, Sumith Kulal, Viktor Kuncak |
| 2017 | Analyzing divergence in bisimulation semantics. | Xinxin Liu, Tingting Yu, Wenhui Zhang |
| 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 | Semantic-directed clumping of disjunctive abstract states. | Huisong Li, Francois Berenger, Bor-Yuh Evan Chang, Xavier Rival |
| 2017 | Contextual isomorphisms. | Paul Blain Levy |
| 2017 | Type directed compilation of row-typed algebraic effects. | Daan Leijen |