Abstract is missing.
- Higher Order Differential Calculus in MathlibSébastien Gouëzel. 1-14 [doi]
- Bar Inductive Predicates for Constructive Algebra in RocqDominique Larchey-Wendling. 15-28 [doi]
- Computing Solutions for Systems of Multivariate Ordinary Differential Equations in RocqHolger Thies. 29-44 [doi]
- Cylindrical Algebraic Decomposition in Coq/RocqQuentin Vermande. 45-58 [doi]
- Adhesive Category Theory for Graph Rewriting in RocqSamuel Arsac, Russ Harmer, Damien Pous. 59-74 [doi]
- Formalizing Polynomial Laws and the Universal Divided Power AlgebraAntoine Chambert-Loir, María Inés de Frutos-Fernández. 75-87 [doi]
- A Certifying Proof Assistant for Synthetic Mathematics in LeanWojciech Nawrocki, Joseph Hua, Mario Carneiro, Yiming Xu, Spencer Woolfson, Shuge Rong, Sina Hazratpour, Steve Awodey. 88-103 [doi]
- Adding Sorts to an Isabelle Formalization of SuperpositionBalázs Tóth, Martin Desharnais-Schäfer, Jasmin Blanchette. 104-116 [doi]
- A Lambda-Superposition Tactic for Isabelle/HOLMassin Guerdi. 117-127 [doi]
- Certifying the Decidability of the Word Problem in Monoids at LargeReinis Cirpons, Florent Hivert, Assia Mahboubi, Guillaume Melquiond, James D. Mitchell, Finn Smith. 128-142 [doi]
- Mechanized Dominator Tree CertificationJean-Christophe Léchenet. 143-156 [doi]
- Brack: A Verified Compiler for Scheme via CakeMLPascal Y. Lasnier, Jeremy Yallop, Magnus O. Myreen. 157-170 [doi]
- Verified VCG and Verified Compiler for DafnyDaniel Nezamabadi, Magnus O. Myreen, Yong Kiam Tan. 171-186 [doi]
- Foundational Verification of Running-Time Bounds for Interactive ProgramsAndy Tockman, Pratap Singh, Andres Erbsen, Samuel Gruetter, Adam Chlipala. 187-200 [doi]
- Can We Formalise Type Theory Intrinsically without Any Compromise? A Case Study in Cubical AgdaLiang-TIng Chen 0001, Fredrik Nordvall Forsberg, Tzu-Chun Tsai. 201-215 [doi]
- Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental FunctionsTomaz Mascarenhas, Harun Khan 0001, Abdalrhman Mohamed, Andrew Reynolds 0001, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli. 216-230 [doi]
- Mechanizing Synthetic Tait Computability in IstariRunming Li, Yue Yao, Robert Harper 0001. 231-247 [doi]
- Building Blocks for Step-Indexed Program LogicsThomas Somers 0001, Jonas Kastberg Hinrichsen, Lennard Gäher, Robbert Krebbers. 248-263 [doi]
- A Rose Tree Is Blooming (Proof Pearl)Joomy Korkut. 264-278 [doi]
- Certified Symbolic Finite Transducers: Formalization and Applications to String AnalysisShuanglong Kan, Anthony W. Lin. 279-293 [doi]
- Enhancing Symbolic Execution with Machine-Checked Safety ProofsDavid Trabish, Shachar Itzhaky. 294-308 [doi]
- Layers of Confluence for ActorsLudovic Henrio, Einar Broch Johnsen, Åsmund Aqissiaq Arild Kløvstad, Violet Ka I Pun, Yannick Zakowski. 309-324 [doi]
- Towards Composable Proofs of Cache Coherence ProtocolsMartina Camaioni, Yann Herklotz, Tz-Ching Yu, Thomas Bourgeat. 325-338 [doi]
- A Recipe for Modular Verification of Generic Tree TraversalsLaila Elbeheiry, Michael Sammler, Robbert Krebbers, Derek Dreyer, Deepak Garg 0001. 339-352 [doi]
- Precise Reasoning about Container-Internal Pointers with Logical PinningYawen Guan, Clément Pit-Claudel. 353-367 [doi]
- Modular Specifications and Implementations of Random Samplers in Higher-Order Separation LogicVirgil Marionneau, Félix Sassus Bourda, Alejandro Aguirre 0001, Lars Birkedal. 368-382 [doi]
- Using Ghost Ownership to Verify Union-Find and Persistent Arrays in RustArnaud Golfouse, Armaël Guéneau, Jacques-Henri Jourdan. 383-397 [doi]