| 2017 | Abstract Specifications for Concurrent Maps. | Shale Xiong, Pedro da Rocha Pinto, Gian Ntzik, Philippa Gardner |
| 2017 | Modular Verification of Procedure Equivalence in the Presence of Memory Allocation. | Tim Wood, Sophia Drossopoulou, Shuvendu K. Lahiri, Susan Eisenbach |
| 2017 | A Higher-Order Logic for Concurrent Termination-Preserving Refinement. | Joseph Tassarotti, Ralf Jung, Robert Harper |
| 2017 | Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization. | Hao Tang, Di Wang, Yingfei Xiong, Lingming Zhang, Xiaoyin Wang, Lu Zhang |
| 2017 | Commutative Semantics for Probabilistic Programming. | Sam Staton |
| 2017 | Modular Verification of Higher-Order Functional Programs. | Ryosuke Sato, Naoki Kobayashi |
| 2017 | Context-Free Session Type Inference. | Luca Padovani |
| 2017 | A Classical Sequent Calculus with Dependent Types. | tienne Miquey |
| 2017 | The Essence of Functional Programming on Semantic Data. | Martin Leinberger, Ralf Lmmel, Steffen Staab |
| 2017 | Probabilistic Termination by Monadic Affine Sized Typing. | Ugo Dal Lago, Charles Grellois |
| 2017 | Comprehending Isabelle/HOL's Consistency. | Ondrej Kuncar, Andrei Popescu |
| 2017 | The Essence of Higher-Order Concurrent Separation Logic. | Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal |
| 2017 | The Power of Non-determinism in Higher-Order Implicit Complexity - Characterising Complexity Classes Using Non-deterministic Cons-Free Programming. | Cynthia Kop, Jakob Grue Simonsen |
| 2017 | Proving Linearizability Using Partial Orders. | Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew J. Parkinson |
| 2017 | Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic. | Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger |
| 2017 | Verified Characteristic Formulae for CakeML. | Armal Guneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish |
| 2017 | APLicative Programming with Naperian Functors. | Jeremy Gibbons |
| 2017 | LINCX: A Linear Logical Framework with First-Class Contexts. | Ana Linn Georges, Agata Murawska, Shawn Otis, Brigitte Pientka |
| 2017 | Extensible Datasort Refinements. | Jana Dunfield |
| 2017 | Tackling Real-Life Relaxed Concurrency with FSL++. | Marko Doko, Viktor Vafeiadis |
| 2017 | Caper - Automatic Verification for Fine-Grained Concurrency. | Thomas Dinsdale-Young, Pedro da Rocha Pinto, Kristoffer Just Andersen, Lars Birkedal |
| 2017 | Is Your Software on Dope? - Formal Analysis of Surreptitiously "enhanced" Programs. | Pedro R. D'Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns |
| 2017 | Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring. | Ryan Culpepper, Andrew Cobb |
| 2017 | Metric Reasoning About \lambda -Terms: The General Case. | Raphalle Crubill, Ugo Dal Lago |
| 2017 | ML and Extended Branching VASS. | Conrad Cotton-Barratt, Andrzej S. Murawski, C.-H. Luke Ong |