| 2020 | Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types. | Sung-Shik Jongmans, Nobuko Yoshida |
| 2020 | SMT-Friendly Formalization of the Solidity Memory Model. | kos Hajdu, Dejan Jovanovic |
| 2020 | Liberate Abstract Garbage Collection from the Stack by Decomposing the Heap. | Kimball Germane, Michael D. Adams |
| 2020 | Soundness Conditions for Big-Step Semantics. | Francesco Dagnino, Viviana Bono, Elena Zucca, Mariangiola Dezani-Ciancaglini |
| 2020 | Concise Read-Only Specifications for Better Synthesis of Programs with Pointers. | Andreea Costea, Amy Zhu, Nadia Polikarpova, Ilya Sergey |
| 2020 | Optimal and Perfectly Parallel Algorithms for On-demand Data-Flow Analysis. | Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis |
| 2020 | Constructive Game Logic. | Rose Bohrer, Andr Platzer |
| 2020 | On the Versatility of Open Logical Relations - Continuity, Automatic Differentiation, and a Containment Theorem. | Gilles Barthe, Raphalle Crubill, Ugo Dal Lago, Francesco Gavazzo |
| 2020 | Runners in Action. | Danel Ahman, Andrej Bauer |
| 2020 | Trace-Relating Compiler Correctness and Secure Compilation. | Carmine Abate, Roberto Blanco, Stefan Ciobaca, Adrien Durier, Deepak Garg, Catalin Hritcu, Marco Patrignani, ric Tanter, Jrmy Thibault |
| 2020 | RustHorn: CHC-Based Verification for Rust Programs. | Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi |
| 2019 | Composing Bidirectional Programs Monadically. | Li-yao Xia, Dominic Orchard, Meng Wang |
| 2019 | One Step at a Time - A Functional Derivation of Small-Step Evaluators from Big-Step Counterparts. | Ferdinand Vesely, Kathleen Fisher |
| 2019 | Handling Polymorphic Algebraic Effects. | Taro Sekiyama, Atsushi Igarashi |
| 2019 | A Categorical Model of an \mathbf i/o -typed \pi -calculus. | Ken Sakayori, Takeshi Tsukada |
| 2019 | Robustly Safe Compilation. | Marco Patrignani, Deepak Garg |
| 2019 | Time Credits and Time Receipts in Iris. | Glen Mvel, Jacques-Henri Jourdan, Franois Pottier |
| 2019 | Extended Call-by-Push-Value: Reasoning About Effectful Programs and Evaluation Order. | Dylan McDermott, Alan Mycroft |
| 2019 | Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms. | Guido Martnez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clment Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy |
| 2019 | Effectful Normal Form Bisimulation. | Ugo Dal Lago, Francesco Gavazzo |
| 2019 | Safe Deferred Memory Reclamation with Types. | Ismail Kuru, Colin S. Gordon |
| 2019 | An Abstract Domain for Trees with Numeric Relations. | Matthieu Journault, Antoine Min, Abdelraouf Ouadjaout |
| 2019 | A Process Algebra for Link Layer Protocols. | Rob van Glabbeek, Peter Hfner, Michael Markl |
| 2019 | Verifiable Certificates for Predicate Subtyping. | Frdric Gilbert |
| 2019 | Incremental \lambda -Calculus in Cache-Transfer Style - Static Memoization by Program Transformation. | Paolo G. Giarrusso, Yann Rgis-Gianas, Philipp Schuster |