Table of Contents

• Fermat's Last Theorem for Regular Primes (Short Paper)Alex J. Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi. [doi]
• Formalizing Functions as ProcessesBeniamino Accattoli, Horace Blanc, Claudio Sacerdoti Coen. [doi]
• MizAR 60 for Mizar 50Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz 0001, Martin Suda 0001, Josef Urban. [doi]
• LISA - A Modern Proof SystemSimon Guilloud, Sankalp Gambhir, Viktor Kuncak. [doi]
• Reimplementing Mizar in RustMario Carneiro. [doi]
• Automated Theorem Proving for MetamathMario Carneiro, Chad E. Brown, Josef Urban. [doi]
• Formalising the Proj Construction in LeanJujian Zhang. [doi]
• Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk)Angeliki Koutsoukou Argyraki. [doi]
• An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any CharacteristicDavid Kurniadi Angdinata, Junyan Xu. [doi]
• Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)Akihisa Yamada 0002, Jérémy Dubut. [doi]
• Real-Time Double-Ended Queue Verified (Proof Pearl)Balázs Tóth, Tobias Nipkow. [doi]
• Fast, Verified Computation for CandleOskar Abrahamsson, Magnus O. Myreen. [doi]
• Now It Compiles! Certified Automatic Repair of Uncompilable ProtocolsLuís Cruz-Filipe, Fabrizio Montesi. [doi]
• A Formalisation of Gallagher's Ergodic TheoremOliver Nash. [doi]
• Closure Properties of General Grammars - Formally VerifiedMartin Dvorak, Jasmin Blanchette. [doi]
• POSIX Lexing with Bitcoded DerivativesChengsong Tan, Christian Urban. [doi]
• Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair DatasetTom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner, Talia Ringer. [doi]
• A Proof-Producing Compiler for Blockchain ApplicationsJeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman. [doi]
• Slice NondeterminismNiels F. W. Voorneveld. [doi]
• Foundational Verification of Stateful P4 Packet ProcessingQinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, Andrew W. Appel. [doi]
• Lessons for Interactive Theorem Proving Researchers from a Survey of Coq UsersAna de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, Théo Zimmermann. [doi]
• Constructive Final Semantics of Finite BagsPhilipp Joram, Niccolò Veltri. [doi]
• No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM SystemRoger Bosman, Georgios Karachalias, Tom Schrijvers. [doi]
• Group Cohomology in the Lean Community LibraryAmelia Livingston. [doi]
• Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOLMichikazu Hirata, Yasuhiko Minamide, Tetsuya Sato 0001. [doi]
• Dependently Sorted Theorem Proving for Mathematical FoundationsYiming Xu, Michael Norrish. [doi]
• A Sound and Complete Projection for Global TypesDawit Legesse Tirore, Jesper Bengtson, Marco Carbone. [doi]
• A Formal Analysis of RANKINGMohammad Abdulaziz, Christoph Madlener. [doi]
• Formalizing Almost Development Closed Critical Pairs (Short Paper)Christina Kohl, Aart Middeldorp. [doi]
• Formalizing Norm Extensions and Applications to Number TheoryMaría Inés de Frutos-Fernández. [doi]
• Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in CoqDominique Larchey-Wendling, Jean-François Monin. [doi]
• Implementing More Explicit Definitional Expansions in Mizar (Short Paper)Adam Grabowski, Artur Kornilowicz. [doi]
• Tealeaves: Structured Monads for Generic First-Order Abstract Syntax InfrastructureLawrence Dunn, Val Tannen, Steve Zdancewic. [doi]
• Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof AssistantPierre Pomeret-Coquot, Hélène Fargier, Érik Martin-Dorel. [doi]
• Interactive and Automated Proofs in Modal Separation Logic (Invited Talk)Robbert Krebbers. [doi]
• Front Matter, Table of Contents, Preface, Conference Organization [doi]
• Certifying Higher-Order Polynomial InterpretationsNiels van der Weide, Deivid Vale, Cynthia Kop. [doi]
• An Extensible User Interface for Lean 4Wojciech Nawrocki, Edward W. Ayers, Gabriel Ebner. [doi]
• Formalising Yoneda Ext in Univalent FoundationsJarl G. Taxerås Flaten. [doi]