The readings shared in Mastodon on September 6, 2024 are

• Readings shared September 5, 2024. #ITP #LeanProver #Lean4 #IsabelleHO #Agda #Logic #Math #Calculemus #Haskell #OCaml #FunctionalProgramming #AI
• Towards solid abelian groups: A formal proof of Nöbeling’s theorem. ~ Dagur Asgeirsson. #ITP #LeanProver #Math
• The directed Van Kampen theorem in Lean. ~ Henning Basold, Peter Bruin & Dominique Lawson. #ITP #LeanProver #Lean4 #Math
• Verifying peephole rewriting in SSA compiler IRs. ~ Siddharth Bhat, Alex Keizer, Chris Hughes, Andrés Goens & Tobias Grosser. #ITP #LeanProver
• Duper: A proof-producing superposition theorem prover for dependent type theory. ~ Joshua Clune, Yicheng Qian, Alexander Bentkamp & Jeremy Avigad. #ITP #LeanProver #Lean4
• Teaching mathematics using Lean and controlled natural language. ~ Patrick Massot. #ITP #LeanProver #Lean4 #Math
• Lean formalization of completeness proof for Coalition Logic with Common Knowledge. ~ Kai Obendrauf, Anne Baanen, Patrick Koopmann & Vera Stebletsova. #ITP #LeanProver #Lean4
• Formal verification of the empty hexagon number. ~ Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro & Marijn J. H. Heule. #ITP #LeanProver #Lean4
• Integrals within integrals: A formalization of the Gagliardo-Nirenberg-Sobolev inequality. ~ Floris van Doorn & Heather Macbeth. #ITP #LeanProver #Lean4 #Math
• Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4. ~ Sam Ezeh. #ITP #LeanProver #Lean4 #Math
• Formalising half of a graduate textbook on number theory. ~ Manuel Eberl, Anthony Bordg, Lawrence C. Paulson & Wenda Li. #ITP #IsabelleHOL #Math
• A formalization of the Lévy-Prokhorov metric in Isabelle/HOL. ~ Michikazu Hirata. #ITP #IsabelleHOL #Math
• Alpha-beta pruning verified. ~ Tobias Nipkow. #ITP #IsabelleHOL
• A formal analysis of capacity scaling algorithms for minimum cost flows. ~ Mohammad Abdulaziz & Thomas Ammer. #ITP #IsabelleHOL
• An operational semantics in Isabelle/HOL-CSP. ~ Benoît Ballenghien & Burkhart Wolff. #ITP #IsabelleHOL
• A verified earley parser. ~ Martin Rau & Tobias Nipkow. #ITP #IsabelleHOL
• A modular formalization of superposition in Isabelle/HOL. ~ Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette & Sophie Tourret. #ITP #IsabelleHOL
• Distributed parallel build for the Isabelle Archive of Formal Proofs. ~ Fabian Huch & Makarius Wenzel. #ITP #IsabelleHOL
• A generalised union of rely–guarantee and separation logic using permission algebras. ~ Vincent Jackson, Toby Murray & Christine Rizkallah. #ITP #IsabelleHOL
• An Isabelle/HOL formalization of narrowing and multiset narrowing for E-unifiability, reachability and infeasibility. ~ Dohan Kim. #ITP #IsabelleHOL
• A Coq formalization of Taylor models and power series for solving ordinary differential equations. ~ Sewon Park & Holger Thies. #ITP #Coq #Math
• A comprehensive overview of the Lebesgue differentiation theorem in Coq. ~ Reynald Affeldt & Zachary Stone. #ITP #Coq #Math
• Taming differentiable logics with Coq formalisation. ~ Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz & Kathrin Stark. #ITP #Coq #Logic #MachineLearning
• Completeness of asynchronous session tree subtyping in Coq. ~ Burak Ekici & Nobuko Yoshida. #ITP #Coq
• End-to-end formal verification of a fast and accurate floating-point approximation. ~ Florian Faissole, Paul Geneau de Lamarlière & Guillaume Melquiond. #ITP #Coq
• Typed compositional quantum computation with lenses. ~ Jacques Garrigue & Takafumi Saikawa. #ITP #Coq
• Verifying software emulation of an unsupported hardware instruction. ~ Samuel Gruetter, Thomas Bourgeat & Adam Chlipala. #ITP #Coq
• Modular verification of intrusive list and tree data structures in separation logic. ~ Marc Hermes & Robbert Krebbers. #ITP #Coq
• Formalizing the algebraic small object argument in UniMath. ~ Dennis Hilhorst & Paige Randall North. #ITP #Coq #Math
• The Rewster: Type preserving rewrite rules for the Coq proof assistant. ~ Yann Leray, Gaëtan Gilbert, Nicolas Tabareau & Théo Winterhalter. #ITP #Coq
• Correctly compiling proofs about programs without proving compilers correct. ~ Audrey Seo, Christopher Lam, Dan Grossman & Talia Ringer. #ITP #Coq
• Redex2Coq: Towards a theory of decidability of redex’s reduction semantics. ~ Mallku Soldevila, Rodrigo Ribeiro & Beta Ziliani. #ITP #Coq
• Defining and preserving more C behaviors: Verified compilation using a concrete memory model. ~ Andrew Tolmach, Chris Chhak & Sean Anderson. #ITP #Coq
• Robust mean estimation by all means. ~ Reynald Affeldt, Clark Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa & Carsten Schürmann. #ITP #Coq
• Abstractions for multi-sorted substitutions. ~ Hannes Saffrich. #ITP #Agda
• The functor of points approach to schemes in Cubical Agda. ~ Max Zeuner & Matthias Hutzler. #ITP #Agda
• A formalization of the general theory of quaternions. ~ Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro & Mauricio Ayala-Rincón. #ITP #PVS #Math
• Formalizing the Cholesky factorization theorem. ~ Carl Kwan & Warren A. Hunt Jr. #ITP #ACL2 #Math
• A formal proof of R(4,5)=25. ~ Thibault Gauthier & Chad E. Brown. #ITP #HOL4 #Math
• Mechanized HOL reasoning in set theory. ~ Simon Guilloud, Sankalp Gambhir, Andrea Gilot & Viktor Kunčak. #ITP #Lisa #Math
• Conway normal form: Bridging approaches for comprehensive formalization of surreal numbers. ~ Karol Pąk & Cezary Kaliszyk. #ITP #Mizar #Math
• 15th International Conference on Interactive Theorem Proving (ITP 2024,). #ITP
• The code of Mathematics: Proof and truth ~ Stefan Müller-Stach. #Math
• Neuro-symbolic theorem proving with Lean. ~ Peiyang Song (@p_song1). #ITP #LeanProver #AI #MachineLearning