| 2020 | A First-Order Logic with Frames. Adithya Murali, Lucas Peña, Christof Löding, P. Madhusudan |
| 2020 | ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures. Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, Peter Sewell |
| 2020 | Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, Lars Birkedal |
| 2020 | ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs. John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, Naoki Kobayashi |
| 2020 | Concise Read-Only Specifications for Better Synthesis of Programs with Pointers. Andreea Costea, Amy Zhu, Nadia Polikarpova, Ilya Sergey |
| 2020 | Connecting Higher-Order Separation Logic to a First-Order Outside World. William Mansky, Wolf Honoré, Andrew W. Appel |
| 2020 | Constructive Game Logic. Rose Bohrer, André Platzer |
| 2020 | Continualization of Probabilistic Programs With Correction. Jacob Laurel, Sasa Misailovic |
| 2020 | Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types. Sung-Shik Jongmans, Nobuko Yoshida |
| 2020 | Higher-Order Spreadsheets with Spilled Arrays. Jack Williams, Nima Joharizadeh, Andrew D. Gordon, Advait Sarkar |
| 2020 | Higher-Ranked Annotation Polymorphic Dependency Analysis. Fabian Thorand, Jurriaan Hage |
| 2020 | Liberate Abstract Garbage Collection from the Stack by Decomposing the Heap. Kimball Germane, Michael D. Adams |
| 2020 | Local Reasoning for Global Graph Properties. Siddharth Krishna, Alexander J. Summers, Thomas Wies |
| 2020 | Mixed Sessions. Vasco T. Vasconcelos, Filipe Casal, Bernardo Almeida, Andreia Mordido |
| 2020 | Modular Inference of Linear Types for Multiplicity-Annotated Arrows. Kazutaka Matsuda |
| 2020 | Modular Relaxed Dependencies in Weak Memory Concurrency. Marco Paviotti, Simon Cooksey, Anouk Paradis, Daniel Wright, Scott Owens, Mark Batty |
| 2020 | On the Versatility of Open Logical Relations - Continuity, Automatic Differentiation, and a Containment Theorem. Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo |
| 2020 | Optimal and Perfectly Parallel Algorithms for On-demand Data-Flow Analysis. Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis |
| 2020 | Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings Peter Müller |
| 2020 | Proving the Safety of Highly-Available Distributed Objects. Sreeja S. Nair, Gustavo Petri, Marc Shapiro |
| 2020 | Runners in Action. Danel Ahman, Andrej Bauer |
| 2020 | RustHorn: CHC-Based Verification for Rust Programs. Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi |
| 2020 | SMT-Friendly Formalization of the Solidity Memory Model. Ákos Hajdu, Dejan Jovanovic |
| 2020 | Semantic Foundations for Deterministic Dataflow and Stream Processing. Konstantinos Mamouras |
| 2020 | Solving Program Sketches with Large Integer Values. Rong Pan, Qinheping Hu, Rishabh Singh, Loris D'Antoni |
| 2020 | Soundness Conditions for Big-Step Semantics. Francesco Dagnino, Viviana Bono, Elena Zucca, Mariangiola Dezani-Ciancaglini |
| 2020 | Trace-Relating Compiler Correctness and Secure Compilation. Carmine Abate, Roberto Blanco, Stefan Ciobaca, Adrien Durier, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter, Jérémy Thibault |
| 2020 | Verifying Visibility-Based Weak Consistency. Siddharth Krishna, Michael Emmi, Constantin Enea, Dejan Jovanovic |