Table of Contents

• Lean Formalization of Completeness Proof for Coalition Logic with Common KnowledgeKai Obendrauf, Anne Baanen, Patrick Koopmann, Vera Stebletsova. [doi]
• A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost FlowsMohammad Abdulaziz, Thomas Ammer. [doi]
• Redex2Coq: Towards a Theory of Decidability of Redex's Reduction SemanticsMallku Soldevila, Rodrigo Geraldo Ribeiro, Beta Ziliani. [doi]
• Teaching Mathematics Using Lean and Controlled Natural LanguagePatrick Massot. [doi]
• Towards Solid Abelian Groups: A Formal Proof of Nöbeling's TheoremDagur Asgeirsson. [doi]
• Abstractions for Multi-Sorted SubstitutionsHannes Saffrich. [doi]
• Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory ModelAndrew Tolmach, Chris Chhak, Sean Noble Anderson. [doi]
• Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal NumbersKarol Pak, Cezary Kaliszyk. [doi]
• Verifying Peephole Rewriting in SSA Compiler IRsSiddharth Bhat, Alex C. Keizer, Chris Hughes, Andrés Goens, Tobias Grosser. [doi]
• Formalizing the Algebraic Small Object Argument in UniMathDennis Hilhorst, Paige Randall North. [doi]
• Completeness of Asynchronous Session Tree Subtyping in CoqBurak Ekici, Nobuko Yoshida. [doi]
• Front Matter, Table of Contents, Preface, Conference Organization [doi]
• A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOLMichikazu Hirata. [doi]
• Mechanized HOL Reasoning in Set TheorySimon Guilloud, Sankalp Gambhir, Andrea Gilot, Viktor Kuncak. [doi]
• Robust Mean Estimation by All Means (Short Paper)Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schürmann. [doi]
• Verifying Software Emulation of an Unsupported Hardware InstructionSamuel Gruetter, Thomas Bourgeat, Adam Chlipala. [doi]
• Modular Verification of Intrusive List and Tree Data Structures in Separation LogicMarc Hermes, Robbert Krebbers. [doi]
• A Formalization of the General Theory of QuaternionsThaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro, Mauricio Ayala-Rincón. [doi]
• End-To-End Formal Verification of a Fast and Accurate Floating-Point ApproximationFlorian Faissole, Paul Geneau de Lamarlière, Guillaume Melquiond. [doi]
• Distributed Parallel Build for the Isabelle Archive of Formal ProofsFabian Huch, Makarius Wenzel. [doi]
• Correctly Compiling Proofs About Programs Without Proving Compilers CorrectAudrey Seo, Christopher Lam 0003, Dan Grossman, Talia Ringer. [doi]
• Formalizing the Cholesky Factorization TheoremCarl Kwan, Warren A. Hunt Jr.. [doi]
• An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and InfeasibilityDohan Kim 0001. [doi]
• The Functor of Points Approach to Schemes in Cubical AgdaMax Zeuner, Matthias Hutzler. [doi]
• Alpha-Beta Pruning Verified (Invited Talk)Tobias Nipkow. [doi]
• A Verified Earley ParserMartin Rau, Tobias Nipkow. [doi]
• An Operational Semantics in Isabelle/HOL-CSPBenoît Ballenghien, Burkhart Wolff. [doi]
• The Directed Van Kampen Theorem in LeanHenning Basold, Peter Bruin, Dominique Lawson. [doi]
• Typed Compositional Quantum Computation with LensesJacques Garrigue, Takafumi Saikawa. [doi]
• Formal Verification of the Empty Hexagon NumberBernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden R. Codel, Mario Carneiro, Marijn J. H. Heule. [doi]
• A Formal Proof of R(4, 5)=25Thibault Gauthier, Chad E. Brown. [doi]
• The Rewster: Type Preserving Rewrite Rules for the Coq Proof AssistantYann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter. [doi]
• Formalising Half of a Graduate Textbook on Number Theory (Short Paper)Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, Wenda Li. [doi]
• Taming Differentiable Logics with Coq FormalisationReynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Slusarz, Kathrin Stark. [doi]
• A Generalised Union of Rely-Guarantee and Separation Logic Using Permission AlgebrasVincent Jackson, Toby Murray, Christine Rizkallah. [doi]
• A Comprehensive Overview of the Lebesgue Differentiation Theorem in CoqReynald Affeldt, Zachary Stone. [doi]
• A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential EquationsSewon Park 0001, Holger Thies. [doi]
• A Modular Formalization of Superposition in Isabelle/HOLMartin Desharnais, Balázs Tóth, Uwe Waldmann, Jasmin Blanchette, Sophie Tourret. [doi]
• Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type TheoryJoshua Clune, Yicheng Qian, Alexander Bentkamp, Jeremy Avigad. [doi]
• Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4 (Short Paper)Sam Ezeh. [doi]
• Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev InequalityFloris van Doorn, Heather Macbeth. [doi]
• Translating Libraries of Definitions and Theorems Between Proof Systems (Invited Talk)Frédéric Blanqui. [doi]