| 2021 | An Automated Deductive Verification Framework for Circuit-building Quantum Programs. Christophe Chareton, Sébastien Bardin, François Bobot, Valentin Perrelle, Benoît Valiron |
| 2021 | Automated Termination Analysis of Polynomial Probabilistic Programs. Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács |
| 2021 | Bayesian strategies: probabilistic programs as generalised graphical models. Hugo Paquet |
| 2021 | Checking Robustness Between Weak Transactional Consistency Models. Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea |
| 2021 | Complete trace models of state and control. Guilhem Jaber, Andrzej S. Murawski |
| 2021 | Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages. Daniel Lundén, Johannes Borgström, David Broman |
| 2021 | Coupled Relational Symbolic Execution for Differential Privacy. Gian Pietro Farina, Stephen Chong, Marco Gaboardi |
| 2021 | Data Flow Analysis of Asynchronous Systems using Infinite Abstract Domains. Snigdha Athaiya, Raghavan Komondoor, K. Narayan Kumar |
| 2021 | Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere. Carol Mak, C.-H. Luke Ong, Hugo Paquet, Dominik Wagner |
| 2021 | Do Judge a Test by its Cover - Combining Combinatorial and Property-Based Testing. Harrison Goldstein, John Hughes, Leonidas Lampropoulos, Benjamin C. Pierce |
| 2021 | For a Few Dollars More - Verified Fine-Grained Algorithm Analysis Down to LLVM. Maximilian P. L. Haslbeck, Peter Lammich |
| 2021 | Graded Hoare Logic and its Categorical Semantics. Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Tetsuya Sato |
| 2021 | Graded Modal Dependent Type Theory. Benjamin Moon, Harley Eades III, Dominic Orchard |
| 2021 | Nested Session Types. Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning |
| 2021 | Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings Nobuko Yoshida |
| 2021 | Query Lifting - Language-integrated query for heterogeneous nested collections. Wilmer Ricciotti, James Cheney |
| 2021 | Reverse AD at Higher Types: Pure, Principled and Denotationally Correct. Matthijs Vákár |
| 2021 | Run-time Complexity Bounds Using Squeezers. Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham |
| 2021 | Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols. Alex C. Keizer, Henning Basold, Jorge A. Pérez |
| 2021 | Sound and Complete Concolic Testing for Higher-order Functions. Shu-Hung You, Robert Bruce Findler, Christos Dimoulas |
| 2021 | Strong-Separation Logic. Jens Pagel, Florian Zuleger |
| 2021 | Temporal Refinements for Guarded Recursive Types. Guilhem Jaber, Colin Riba |
| 2021 | The Decidability of Verification under PS 2.0. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole, S. Krishna, Viktor Vafeiadis |
| 2021 | Types for Complexity of Parallel Computation in Pi-Calculus. Patrick Baillot, Alexis Ghyselen |
| 2021 | Verified Software Units. Lennart Beringer |