| 2026 | A Certifying Proof Assistant for Synthetic Mathematics in Lean. Wojciech Nawrocki, Joseph Hua, Mario Carneiro, Yiming Xu, Spencer Woolfson, Shuge Rong, Sina Hazratpour, Steve Awodey |
| 2026 | A Lambda-Superposition Tactic for Isabelle/HOL. Massin Guerdi |
| 2026 | A Recipe for Modular Verification of Generic Tree Traversals. Laila Elbeheiry, Michael Sammler, Robbert Krebbers, Derek Dreyer, Deepak Garg |
| 2026 | A Rose Tree Is Blooming (Proof Pearl). Joomy Korkut |
| 2026 | Adding Sorts to an Isabelle Formalization of Superposition. Balázs Tóth, Martin Desharnais-Schäfer, Jasmin Blanchette |
| 2026 | Adhesive Category Theory for Graph Rewriting in Rocq. Samuel Arsac, Russ Harmer, Damien Pous |
| 2026 | Bar Inductive Predicates for Constructive Algebra in Rocq. Dominique Larchey-Wendling |
| 2026 | Brack: A Verified Compiler for Scheme via CakeML. Pascal Y. Lasnier, Jeremy Yallop, Magnus O. Myreen |
| 2026 | Building Blocks for Step-Indexed Program Logics. Thomas Somers, Jonas Kastberg Hinrichsen, Lennard Gäher, 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 |
| 2026 | Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis. Shuanglong Kan, Anthony W. Lin |
| 2026 | Certifying the Decidability of the Word Problem in Monoids at Large. Reinis Cirpons, Florent Hivert, Assia Mahboubi, Guillaume Melquiond, James D. Mitchell, Finn Smith |
| 2026 | Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq. Holger Thies |
| 2026 | Cylindrical Algebraic Decomposition in Coq/Rocq. Quentin Vermande |
| 2026 | Enhancing Symbolic Execution with Machine-Checked Safety Proofs. David Trabish, Shachar Itzhaky |
| 2026 | Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions. Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli |
| 2026 | Formalizing Polynomial Laws and the Universal Divided Power Algebra. Antoine Chambert-Loir, María Inés de Frutos-Fernández |
| 2026 | Foundational Verification of Running-Time Bounds for Interactive Programs. Andy Tockman, Pratap Singh, Andres Erbsen, Samuel Gruetter, Adam Chlipala |
| 2026 | Higher Order Differential Calculus in Mathlib. Sébastien Gouëzel |
| 2026 | Layers of Confluence for Actors. Ludovic Henrio, Einar Broch Johnsen, Åsmund Aqissiaq Arild Kløvstad, Violet Ka I Pun, Yannick Zakowski |
| 2026 | Mechanized Dominator Tree Certification. Jean-Christophe Léchenet |
| 2026 | Mechanizing Synthetic Tait Computability in Istari. Runming Li, Yue Yao, Robert Harper |
| 2026 | Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic. Virgil Marionneau, Félix Sassus Bourda, Alejandro Aguirre, Lars Birkedal |
| 2026 | Precise Reasoning about Container-Internal Pointers with Logical Pinning. Yawen Guan, Clément Pit-Claudel |
| 2026 | Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2026, Rennes, France, January 12-13, 2026 Kathrin Stark, Yannick Zakowski, Nikhil Swamy, Nicolas Tabareau |
| 2026 | Towards Composable Proofs of Cache Coherence Protocols. Martina Camaioni, Yann Herklotz, Tz-Ching Yu, Thomas Bourgeat |
| 2026 | Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust. Arnaud Golfouse, Armaël Guéneau, Jacques-Henri Jourdan |
| 2026 | Verified VCG and Verified Compiler for Dafny. Daniel Nezamabadi, Magnus O. Myreen, Yong Kiam Tan |