| 2026 | Building Blocks for Step-Indexed Program Logics. | Thomas Somers, Jonas Kastberg Hinrichsen, Lennard Gher, Robbert Krebbers |
| 2026 | Can We Formalise Type Theory Intrinsically without Any Compromise? A Case Study in Cubical Agda. | Liang-Ting Chen, Fredrik Nordvall Forsberg, Tzu-Chun Tsai |
| 2025 | A CHERI C Memory Model for Verified Temporal Safety. | Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida, Nathaniel Wesley Filardo, Ian Stark, Peter Sewell |
| 2025 | Split Decisions: Explicit Contexts for Substructural Languages. | Daniel Zackon, Chuta Sano, Alberto Momigliano, Brigitte Pientka |
| 2025 | The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic. | Simon Friis Vindum, Ana Linn Georges, Lars Birkedal |
| 2025 | Nominal Matching Logic with Fixpoints. | Mircea Sebe, Maribel Fernndez, James Cheney |
| 2025 | Prospects for Computer Formalization of Infinite-Dimensional Category Theory (Invited Talk). | Emily Riehl |
| 2025 | Formally Verified Hardening of C Programs against Hardware Fault Injection. | Basile Pesin, Sylvain Boulm, David Monniaux, Marie-Laure Potet |
| 2025 | Further Tackling Post Correspondence Problem and Proof Generation. | Akihiro Omori, Yasuhiko Minamide |
| 2025 | CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq. | Wolfgang Meier, Martin Jensen, Jean Pichon-Pharabod, Bas Spitters |
| 2025 | Tactic Script Optimisation for Aesop. | Jannis Limperg |
| 2025 | Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems. | Christina Kirk, Aart Middeldorp |
| 2025 | CRIS: The Power of Imagination in Specification and Verification (Invited Talk). | Chung-Kil Hur |
| 2025 | Machine Checked Proofs and Programs in Algebraic Combinatorics. | Florent Hivert |
| 2025 | Formalizing the One-Way to Hiding Theorem. | Katharina Heidler, Dominique Unruh |
| 2025 | An Isabelle/HOL Framework for Synthetic Completeness Proofs. | Asta Halkjr From |
| 2025 | Formalized Burrows-Wheeler Transform. | Louis Cheung, Alistair Moffat, Christine Rizkallah |
| 2025 | Verified and Efficient Matching of Regular Expressions with Lookaround. | Agnishom Chattopadhyay, Angela W. Li, Konstantinos Mamouras |
| 2025 | Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR. | Nicolas Chappe, Ludovic Henrio, Yannick Zakowski |
| 2025 | Certifying Rings of Integers in Number Fields. | Anne Baanen, Alain Chavarri Villarello, Sander R. Dahmen |
| 2025 | Leakage-Free Probabilistic Jasmin Programs. | Jos Bacelar Almeida, Denis Firsov, Tiago Oliveira, Dominique Unruh |
| 2025 | Intrinsically Correct Sorting in Cubical Agda. | Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, Niels van der Weide |
| 2025 | An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting. | Dohan Kim, Teppei Saito, Ren Thiemann, Akihisa Yamada |
| 2025 | Formalization of Differential Privacy in Isabelle/HOL. | Tetsuya Sato, Yasuhiko Minamide |
| 2024 | Lean Formalization of Extended Regular Expression Matching with Lookarounds. | Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner |