Invited Speakers

• Frédéric Blanqui (INRIA),
• Tobias Nipkow (Technical University of Munich),

Tutorial

• Evgenia Karunus, Visualising Mathematical Proof: Paperproof

List of Accepted Papers

• Mohammad Abdulaziz and Thomas Ammer, A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows
• Reynald Affeldt, Clark Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa and Carsten Schürmann, Robust mean estimation by all means (short paper)
• Reynald Affeldt and Zachary Stone, A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq
• Dagur Asgeirsson, Towards solid abelian groups: A formal proof of Nöbeling's theorem
• Benoît Ballenghien and Burkhart Wolff, An Operational Semantics in Isabelle/HOL-CSP
• Henning Basold, Peter Bruin and Dominique Lawson, The Directed Van Kampen Theorem in Lean
• Siddharth Bhat, Alex Keizer, Chris Hughes, Andres Goens and Tobias Grosser, Verifying Peephole Rewriting In SSA Compiler IRs
• Joshua Clune, Yicheng Qian, Alexander Bentkamp and Jeremy Avigad, Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory
• Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro and Mauricio Ayala-Rincón, A Formalization of the General Theory of Quaternions
• Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette and Sophie Tourret, A Modular Formalization of Superposition in Isabelle/HOL
• Manuel Eberl, Anthony Bordg, Lawrence Paulson and Wenda Li, Formalising Half of a Graduate Textbook on Number Theory
• Burak Ekici and Nobuko Yoshida, Completeness of Asynchronous Session Tree Subtyping in Coq
• Sam Ezeh, Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4 (Short paper)
• Florian Faissole, Paul Geneau de Lamarlière and Guillaume Melquiond, End-to-End Formal Verification of a Fast and Accurate Floating-Point Approximation
• Jacques Garrigue and Takafumi Saikawa, Typed compositional quantum computation with lenses
• Thibault Gauthier and Chad Brown, A Formal Proof of R(4,5) = 25
• Samuel Gruetter, Thomas Bourgeat and Adam Chlipala, Verifying Software Emulation of an Unsupported Hardware Instruction
• Simon Guilloud, Sankalp Gambhir, Andrea Gilot and Viktor Kuncak, Mechanized Embedding of HOL in Set Theory
• Marc Hermes and Robbert Krebbers, Modular Verification of Intrusive List and Tree Data Structures in Separation Logic
• Dennis Hilhorst and Paige North, Formalizing the algebraic small object argument in UniMath
• Michikazu Hirata, A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL
• Fabian Huch and Makarius Wenzel, Distributed Parallel Build for the Isabelle Archive of Formal Proofs
• Vincent Jackson, Toby Murray and Christine Rizkallah, A Generalised Union of Rely-Guarantee and Separation Logic using Permission Algebras
• Dohan Kim, An Isabelle/HOL formalization of narrowing and multiset narrowing for E-unifiability, reachability and infeasibility
• Carl Kwan and Warren Hunt, Formalizing the Cholesky Factorization Theorem
• Yann Leray, Gaëtan Gilbert, Nicolas Tabareau and Théo Winterhalter, The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant
• Patrick Massot, Teaching mathematics using Lean and controlled natural language
• Kai Obendrauf, Anne Baanen, Patrick Koopmann and Vera Stebletsova, Lean Formalization of a Completeness Proof for Coalition Logic with Common Knowledge
• Karol Pąk and Cezary Kaliszyk, Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers
• Sewon Park and Holger Thies, A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations
• Martin Rau and Tobias Nipkow, A Verified Earley Parser
• Hannes Saffrich, Abstractions for Multi-Sorted Substitutions
• Audrey Seo, Christopher Lam, Dan Grossman and Talia Ringer, Correctly Compiling Proofs About Programs Without Proving Compilers Correct
• Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz and Kathrin Stark, Taming Differentiable Logics With Coq Formalisation
• Mallku Soldevila, Rodrigo Ribeiro and Beta Ziliani, Redex2Coq: towards a theory of decidability of Redex’s reduction semantics
• Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro and Marijn Heule, Formal Verification of the Empty Hexagon Number
• Andrew Tolmach, Chris Chhak and Sean Anderson, Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model
• Floris van Doorn and Heather Macbeth, Integrals within integrals: a formalization of the Gagliardo-Nirenberg-Sobolev inequality
• Max Zeuner and Matthias Hutzler, The Functor of Points Approach to Schemes in Cubical Agda