Invited Speakers:

List of Accepted Papers:

• Mohammad Abdulaziz and Christoph Madlener: A Formal Analysis of RANKING
• Oliver Nash: A formalisation of Gallagher’s ergodic theorem
• Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer and Alon Titelman: A Proof-Producing Compiler for Blockchain Applications
• Dawit Tirore, Jesper Bengtson and Marco Carbone: A Sound and Complete Projection for Global Types
• David Kurniadi Angdinata and Junyan Xu: An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in any Characteristic
• Wojciech Nawrocki, Edward W. Ayers and Gabriel Ebner: An extensible user interface for Lean 4
• Mario Carneiro, Chad Brown and Josef Urban: Automated Theorem Proving for Metamath
• Pierre Pomeret-Coquot, Helene Fargier and Érik Martin-Dorel: Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant
• Niels van der Weide, Deivid Vale and Cynthia Kop: Certifying Higher-Order Polynomial Interpretations
• Martin Dvorak and Jasmin Blanchette: Closure Properties of Unrestricted Grammars — Formally Verified
• Philipp Joram and Niccolò Veltri: Constructive Final Semantics of Finite Bags
• Yiming Xu and Michael Norrish: Dependent Sorted Theorem Proving for Mathematical Foundations
• Oskar Abrahamsson and Magnus O. Myreen: Fast, Verified Computation for Candle
• Alex Best, Christopher Birkbeck, Riccardo Brasca and Eric Rodriguez: Fermat’s Last Theorem for regular primes (short paper)
• Jujian Zhang: Formalising the Proj construction
• Jarl G. Taxeraas Flaten: Formalising Yoneda Ext in Univalent Foundations
• Christina Kohl and Aart Middeldorp: Formalizing Almost Development Closed Critical Pairs (Short Paper)
• Beniamino Accattoli, Horace Blanc and Claudio Sacerdoti Coen: Formalizing Functions as Processes
• María Inés de Frutos-Fernández: Formalizing Norm Extensions and Applications to Number Theory
• Akihisa Yamada and Jérémy Dubut: Formalizing Results on Directed Sets in Isabelle/HOL
• Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer and Andrew W. Appel: Foundational verification of stateful P4 packet processing
• Amelia Livingston: Group cohomology in the Lean community library
• Adam Grabowski and Artur Korniłowicz: Implementing More Explicit Definitional Expansions in Mizar (short paper)
• Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Erik Martin-Dorel, Karl Palmskog, Alexander Serebrenik and Théo Zimmermann: Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users
• Simon Guilloud, Sankalp Gambhir and Viktor Kuncak: LISA - A Proof Assistant Embedded in Scala
• Jan Jakubuv, Karel Chvalovský, Zarathustra Goertzel, Cezary Kaliszyk, Miroslav Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda and Josef Urban: MizAR 60 for Mizar 50
• Roger Bosman, Georgios Karachalias and Tom Schrijvers: No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System
• Luís Cruz-Filipe and Fabrizio Montesi: Now It Compiles! - Certified Automatic Repair of Uncompilable Protocols
• Chengsong Tan and Christian Urban: POSIX Lexing with Bitcoded Derivatives
• Dominique Larchey-Wendling and Jean-Francois Monin: Proof pearl: faithful computation and extraction of µ-recursive algorithms in Coq
• Tom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner and Talia Ringer: Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset
• Balazs Toth and Tobias Nipkow: Real-Time Double-Ended Queue Verified (Proof Pearl)
• Mario Carneiro: Reimplementing Mizar in Rust
• Michikazu Hirata, Yasuhiko Minamide and Tetsuya Sato: Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL
• Niels Voorneveld: Slice Nondeterminism
• Lawrence Dunn, Val Tannen and Steve Zdancewic: Tealeaves: Structured monads for generic first-order abstract syntax infrastructure