Invited Speakers
Tutorial
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