Abstract is missing.
- Panbench: A Comparative Benchmarking Tool for Dependently-Typed LanguagesReed Mullanix, Jacques Carette. [doi]
- Formalizing the Bruck-Ryser-Chowla Theorem: Combinatorial Design Theory in LeanEric Jonathan Wang, Elif Üsküplü. [doi]
- String Diagrams for Monoidal Categories, in RocqDamien Pous. [doi]
- Formally Verified Liveness with Multiparty Session Types in RocqOmer Keskin, Nobuko Yoshida, Rob van Glabbeek. [doi]
- Lean on Vampire Proofs (Short Paper)Jonas Bodingbauer, Márton Hajdú, Laura Kovács, Axel Polaczek, Michael Rawson 0001. [doi]
- Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured IsarSage Binder, Hanna Lachnitt, Katherine Kosaian. [doi]
- Lazy Proof Automation for Separation LogicValentin Mikhalchuk, Vladimir Gladshtein, Ilya Sergey. [doi]
- Formalizing Abstract Simplicial Complexes & Stellar Subdivisions in LeanGarett Cunningham, Daniel Zach, Stefan Friedl. [doi]
- ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-ProvingAmitayush Thakur, George Tsoukalas, Greg Durrett, Swarat Chaudhuri. [doi]
- An End-To-End Verification of Keller's ConjectureJames Gallicchio, Cayden R. Codel, Jeremy Avigad, Marijn J. H. Heule. [doi]
- Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy IntegralSho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda. [doi]
- Securing the Foundations of an Intermediate Language for Probabilistic Program VerificationOliver Bøving, Christoph Matheja. [doi]
- Three Roads to de Finetti's Theorem in Lean 4 (Short Paper)Cameron E. Freer. [doi]
- TableauxRocq: A Deep Embedding of Free-Variable Tableaux in RocqJohann Rosain, Julie Cailler. [doi]
- From Weierstraß to Dedekind via Jacobi: Formalising Foundations of Modular FormsManuel Eberl, Wenda Li 0001, Lawrence C. Paulson. [doi]
- Front Matter, Table of Contents, Preface, Conference Organization [doi]
- Faster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper)Aeacus Sheng, Wenda Li 0001, Paul B. Jackson. [doi]
- Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOLFang Yan 0004, Benoît Ballenghien, Simon Foster 0001, Ana Cavalcanti 0001, James Baxter 0001, Burkhart Wolff. [doi]
- Feedback & Synthesis in LLM-Assisted Termination ProofsZeke Medley, Panagiotis Manolios. [doi]
- Formal Primal-Dual Algorithm Analysis (Short Paper)Mohammad Abdulaziz, Thomas Ammer, Christoph Madlener. [doi]
- Nitro Isolation Engine: Formally Verifying a Production Hypervisor (Invited Talk)Hanno Becker, Nathan Chong, Robert Dockins, Jim Grundy, Jason Z. S. Hu, Ike Mulder, Dominic P. Mulligan, Paul Mure, Bryan Parno, Lawrence C. Paulson, Konrad Slind. [doi]
- A Lean Tactic for Normalizing Expressions in an Algebra over a Ring (Short Paper)Arend Mellendijk. [doi]
- Certified Infinite Descent Criteria in Isabelle/HOLJamie Wright, Liron Cohen 0001, Reuben N. S. Rowe, Andrei Popescu 0001. [doi]
- 130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone? (Short Paper)Josef Urban. [doi]
- Functional Correctness of an Optimized Modular Inversion AlgorithmAssia Mahboubi, Guillaume Melquiond, Pierre-Yves Strub, Tomás Vallejos Parada. [doi]
- Enhancing Interactive Theorem Prover Error Messages with HintsMaria Khakimova, Sára Juhosová, Jaro S. Reinders, Jesper Cockx. [doi]
- Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine EquationsRicardo Almeida 0003, Blair Archibald, Basile Pesin, Michele Sevegnani. [doi]
- Don't Sweat Interaction Trees: Proof-Guided Local Variable Lifting for Interaction TreesYiming Lin, Ian Kariniemi, Yao Li 0004. [doi]
- Fractional Separation Logic in Isabelle LLVMPeter Lammich. [doi]
- Complex Bounded Operators in Isabelle/HOLDominique Unruh, José Manuel Rodríguez Caballero. [doi]
- Formalizing a Hoare Calculus for Choreographic ProgrammingLuís Cruz-Filipe, Thomas Wulff Heissel. [doi]
- Verification of the Garsia-Wachs AlgorithmMakoto Kanazawa. [doi]
- Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification LanguageVladimir Gladshtein, K. Rustan M. Leino. [doi]
- LeanArchitect: Automating Blueprint Generation for Humans and AIThomas Zhu, Pietro Monticone, Sean Welleck, Jeremy Avigad. [doi]
- Bidirectional Interpolation for the λ-Calculus: Revisiting and Formalising Craig-Čubrić InterpolationMeven Lennon-Bertrand, Alexis Saurin. [doi]
- Completing Almost Fair SimulationsArthur Correnson, Iona Kuhn, Bernd Finkbeiner. [doi]
- Developing a Quantum Crypto Theorem Prover from Scratch (Invited Talk)Dominique Unruh. [doi]