| 2017 | A Classical Sequent Calculus with Dependent Types. Étienne Miquey |
| 2017 | A Higher-Order Logic for Concurrent Termination-Preserving Refinement. Joseph Tassarotti, Ralf Jung, Robert Harper |
| 2017 | APLicative Programming with Naperian Functors. Jeremy Gibbons |
| 2017 | Abstract Specifications for Concurrent Maps. Shale Xiong, Pedro da Rocha Pinto, Gian Ntzik, Philippa Gardner |
| 2017 | Caper - Automatic Verification for Fine-Grained Concurrency. Thomas Dinsdale-Young, Pedro da Rocha Pinto, Kristoffer Just Andersen, Lars Birkedal |
| 2017 | Commutative Semantics for Probabilistic Programming. Sam Staton |
| 2017 | Comprehending Isabelle/HOL's Consistency. Ondrej Kuncar, Andrei Popescu |
| 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 | Confluence of Graph Rewriting with Interfaces. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, Fabio Zanasi |
| 2017 | Context-Free Session Type Inference. Luca Padovani |
| 2017 | Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring. Ryan Culpepper, Andrew Cobb |
| 2017 | Disjoint Polymorphism. João Alpuim, Bruno C. d. S. Oliveira, Zhiyuan Shi |
| 2017 | Extensible Datasort Refinements. Jana Dunfield |
| 2017 | Faster Algorithms for Weighted Recursive State Machines. Krishnendu Chatterjee, Bernhard Kragl, Samarth Mishra, Andreas Pavlogiannis |
| 2017 | Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel |
| 2017 | Generalizing Inference Systems by Coaxioms. Davide Ancona, Francesco Dagnino, Elena Zucca |
| 2017 | Incremental Update for Graph Rewriting. Pierre Boutillier, Thomas Ehrhard, Jean Krivine |
| 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 | LINCX: A Linear Logical Framework with First-Class Contexts. Aïna Linn Georges, Agata Murawska, Shawn Otis, Brigitte Pientka |
| 2017 | Linearity, Control Effects, and Behavioral Types. Luís Caires, Jorge A. Pérez |
| 2017 | ML and Extended Branching VASS. Conrad Cotton-Barratt, Andrzej S. Murawski, C.-H. Luke Ong |
| 2017 | Metric Reasoning About \lambda -Terms: The General Case. Raphaëlle Crubillé, Ugo Dal Lago |
| 2017 | Modular Verification of Higher-Order Functional Programs. Ryosuke Sato, Naoki Kobayashi |
| 2017 | Modular Verification of Procedure Equivalence in the Presence of Memory Allocation. Tim Wood, Sophia Drossopoulou, Shuvendu K. Lahiri, Susan Eisenbach |
| 2017 | Observed Communication Semantics for Classical Processes. Robert Atkey |
| 2017 | Probabilistic Termination by Monadic Affine Sized Typing. Ugo Dal Lago, Charles Grellois |
| 2017 | Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings Hongseok Yang |
| 2017 | Programs Using Syntax with First-Class Binders. Francisco Ferreira, Brigitte Pientka |
| 2017 | Proving Linearizability Using Partial Orders. Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew J. Parkinson |
| 2017 | Tackling Real-Life Relaxed Concurrency with FSL++. Marko Doko, Viktor Vafeiadis |
| 2017 | Temporary Read-Only Permissions for Separation Logic. Arthur Charguéraud, François Pottier |
| 2017 | The Essence of Functional Programming on Semantic Data. Martin Leinberger, Ralf Lämmel, Steffen Staab |
| 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 | 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. Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish |
| 2017 | Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency. Ahmed Bouajjani, Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan, Serdar Tasiran |