Invited Speakers

Dominic Mulligan, Amazon Web Services

Dominique Unruh, RWTH Aachen and University of Tartu

Program Schedule

TBA

List of Accepted Papers

• Ricardo Almeida, Blair Archibald, Basile Pesin and Michele Sevegnani. Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations
• Thomas Ammer, Mohammad Abdulaziz and Christoph Madlener. Formal Primal-Dual Algorithm Analysis (Short Paper)
• Sage Binder, Hanna Lachnitt and Katherine Kosaian. Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
• Jonas Bodingbauer, Marton Hajdu, Laura Kovacs, Axel Polaczek and Michael Rawson. Lean on Vampire Proofs (Short Paper)
• Oliver Emil Bøving and Christoph Matheja. Securing the Foundations of an Intermediate Language for Probabilistic Program Verification
• Arthur Correnson, Iona Kuhn and Bernd Finkbeiner. Completing Almost Fair Simulations
• Luís Cruz-Filipe and Thomas Wulff Heissel. Formalizing a Hoare Calculus for Choreographic Programming
• Garett Cunningham, Daniel Zach and Stefan Friedl. Formalizing Abstract Simplicial Complexes & Stellar Subdivisions in Lean
• Manuel Eberl, Wenda Li and Lawrence C. Paulson. From Weierstraß to Dedekind: Formalising Foundations of Modular Forms
• Cameron Freer. Three Roads to de Finetti's Theorem in Lean: Short Paper
• James Gallicchio, Cayden Codel, Jeremy Avigad and Marijn J. H. Heule. An End-to-End Verification of Keller's Conjecture
• Vladimir Gladshtein and K. Rustan M. Leino. Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language
• Makoto Kanazawa. Verification of the Garsia–Wachs Algorithm
• Omer Keskin, Nobuko Yoshida and Rob van Glabbeek. Formally Verified Liveness with Multiparty Session Types in Rocq
• Maria Khakimova, Sára Juhošová, Jaro Reinders and Jesper Cockx. Enhancing Interactive Theorem Prover Error Messages with Hints
• Peter Lammich. Fractional Separation Logic in Isabelle/LLVM
• Meven Lennon-Bertrand and Alexis Saurin. Bidirectional Interpolation for the Lambda-Calculus – Revisiting and Formalising Craig-Čubrić Interpolation
• Yiming Lin, Ian Kariniemi and Yao Li . Don't Sweat Interaction Trees: Proof-Guided Local Variable Lifting for Interaction Trees
• Assia Mahboubi, Guillaume Melquiond, Pierre-Yves Strub and Tomás Vallejos Parada. Functional correctness of an optimized modular inversion algorithm
• Zeke Medley and Panagiotis Manolios. Feedback & Synthesis in LLM-Assisted Termination Proofs
• Arend Mellendijk. A Lean Tactic for Normalizing Expressions in an Algebra over a Ring
• Valentin Mikhalchuk, Vladimir Gladshtein and Ilya Sergey. Lazy Proof Automation for Separation Logic
• Reed Mullanix and Jacques Carette. Panbench: A Comparative Benchmarking Tool for Dependently-Typed Languages
• Damien Pous. String diagrams for monoidal categories, in Rocq
• Johann Rosain and Julie Cailler. TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq
• Aeacus Sheng, Wenda Li and Paul Jackson. Faster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper)
• Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto and Naoto Onda. Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral
• Amitayush Thakur, George Tsoukalas, Greg Durrett and Swarat Chaudhuri. ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
• Dominique Unruh. Complex Bounded Operators in Isabelle/HOL
• Josef Urban. 130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone? (Short Paper)
• Eric Wang and Elif Uskuplu. Formalizing the Bruck-Ryser-Chowla Theorem: Combinatorial Design Theory in Lean
• Jamie Wright, Liron Cohen, Reuben N. S. Rowe and Andrei Popescu. Certified Infinite Descent Criteria in Isabelle/HOL
• Fang Yan, Benoît Ballenghien, Simon Foster, Ana Cavalcanti, James Baxter and Burkhart Wolff. Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL
• Thomas Zhu, Pietro Monticone, Jeremy Avigad and Sean Welleck. LeanArchitect: Automating Blueprint Generation for Humans and AI