| 2024 | A Formalization of Complete Discrete Valuation Rings and Local Fields. María Inés de Frutos-Fernández, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio |
| 2024 | A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic. Ian Shillito, Dominik Kirst |
| 2024 | A Temporal Differential Dynamic Logic Formal Embedding. Lauren M. White, Laura Titolo, J. Tanner Slagel, César A. Muñoz |
| 2024 | Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs. Nao Hirokawa, Dohan Kim, Kiraku Shintani, René Thiemann |
| 2024 | Compositional Verification of Concurrent C Programs with Search Structure Templates. Duc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang |
| 2024 | Displayed Monoidal Categories for the Semantics of Linear Logic. Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert |
| 2024 | Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma. Chelsea Edmonds, Lawrence C. Paulson |
| 2024 | Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture. Siddhartha Gadgil, Anand Rao Tadipatri |
| 2024 | Formalizing the ∞-Categorical Yoneda Lemma. Nikolai Kudasov, Emily Riehl, Jonathan Weinberger |
| 2024 | Lean Formalization of Extended Regular Expression Matching with Lookarounds. Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner |
| 2024 | Martin-Löf à la Coq. Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet |
| 2024 | Memory Simulations, Security and Optimization in a Verified Compiler. David Monniaux |
| 2024 | PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams. Clément Chavanon, Frédéric Besson, Tristan Ninet |
| 2024 | Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024 Amin Timany, Dmitriy Traytel, Brigitte Pientka, Sandrine Blazy |
| 2024 | Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic. Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, Ilya Sergey |
| 2024 | Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments. Joseph Eremondi |
| 2024 | The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters |
| 2024 | UTC Time, Formally Verified. Ana de Almeida Borges, Mireia González Bedmar, Juan José Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, Joost J. Joosten |
| 2024 | Under-Approximation for Scalable Bug Detection (Keynote). Azalea Raad |
| 2024 | Unification for Subformula Linking under Quantifiers. Ike Mulder, Robbert Krebbers |
| 2024 | Univalent Double Categories. Niels van der Weide, Nima Rasekh, Benedikt Ahrens, Paige Randall North |
| 2024 | VCFloat2: Floating-Point Error Analysis in Coq. Andrew W. Appel, Ariel Kellison |