The readings shared in Mastodon on September 9, 2024 are

• Readings shared September 8, 2024. #ITP #Agda #Math #Haskell #FunctionalProgramming
• Proofs of "a+aq+aq²+···+aqⁿ = a(1-qⁿ⁺¹)/(1-q)" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Describing a knight's tour with Prolog. ~ Markus Triska. #Prolog #FunctionalProgramming
• String Knuth Bendix. ~ Philip Zucker. #Math #Python

The readings shared in Mastodon on September 8, 2024 are

• Readings shared September 7, 2024. #ITP #Lean4 #IsabelleHOL #Maude #ATP #Prover9 #Math #Calculemus
• Formalization of the structure sheaf of a ring spectrum. ~ Maša Žaucer. #ITP #Agda #Math
• Automatic test-case generation for Haskell based on dependent types. ~ Pablo Castellanos García. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 7, 2024 are

• Readings shared September 6, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Coq #Agda #PVS #Logic #HOL4 #Lisa #Mizar #ACL2 #Math #AI #MachineLearning
• Proofs of "a+(a+d)+(a+2d)+···+(a+nd) = (n+1)(2a+nd)/2" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Metaprogramming in Lean. ~ Siddhartha Gadgil. #ITP #LeanProver #Lean4
• Examples using MetaProgramming for writing tactics. ~ Siddhartha Gadgil. #ITP #LeanProver #Lean4
• Formalisation of Hall’s theorem for countable infinite graphs. ~ Fabián Fernando Serrano Suárez, Mauricio Ayala-Rincón & Thaynara Arielly de Lima. #ITP #IsabelleHOL #Math
• First-order theorem proving with power maps in semigroups. ~ Yi Lin1, Ranganathan Padmanabhan & Yang Zhang. #ATP #Prover9 #Math
• Maude2Lean: Theorem proving for Maude specifications using Lean. ~ Rubén Rubio & Adrián Riesco. #ITP #Maude #LeanProver #Lean3

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. #ITP #LeanProver #AI #MachineLearning

The readings shared in Mastodon on September 5, 2024 are

• Readings shared September 4, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #Haskell #FunctionalProgramming
• Proofs of "0+1+2+3+···+n=n(n + 1)/2" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Lean: First steps (07 - Proof by cases). ~ Tariq Rashid. #ITP #Lean4 #Math
• Logic and proof. ~ Jeremy Avigad, Robert Y. Lewis & Floris van Doorn. #ITP #LeanProver #Lean4 #Logic #Math
• Formalising inductive and coinductive containers. ~ Stefania Damato, Thorsten Altenkirch & Axel Ljungström.3# #ITP #Agda
• Sized types and coinduction in Safe Agda. ~ Isaac Elliott. #Agda #FunctionalProgramming
• OCaml scientific computing. #OCaml #FunctionalProgramming #AI
• LSP: the good, the bad, and the ugly. ~ Michael Peyton Jones. #Haskell #FunctionalProgramming
• Parsers are relative bimonads. ~ Artemis. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 4, 2024 are

• Readings shared September 3, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Proofs of "If f is continuous at a and the limit of u(n) is a, then the limit of f(u(n)) is f(a)" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Seven levels of type safety in Haskell: Lists. ~ Justin Lê. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 3, 2024 are

• Readings shared September 2, 2024. #ITP #Lean4 #LeanProver #IsabelleHOL #Coq #Maude #Math #Calculemus #FunctionalProgramming
• Proofs of "If x is the limit of u and y is an upper bound of u, then x ≤ y" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• An exponential improvement for diagonal Ramsey (in Isabelle/HOL). ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math
• Extension of stateful intransitive noninterference with inputs, outputs, and nondeterminism in language IMP. ~ Pasquale Noce. #ITP #IsabelleHOL
• Definitive set semantics for LTL3 (in Isabelle/HOL). ~ Rayhana Amjad, Rob van Glabbeek & Liam O’Connor. #ITP #IsabelleHOL

The readings shared in Mastodon on September 2, 2024 are

• Readings shared September 1, 2024. #ITP #Agda
• Proofs of "If (∀ ε > 0, y ≤ x + ε), then y ≤ x" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Maude2Lean: Theorem proving for Maude specifications using Lean. ~ Rubén Rubio & Adrián Riesco. #ITP #LeanProver #Maude
• Scaling the evolution of verified software. ~ Kiran Gopinathan. #PhDThesis #ITP #Coq
• Ramsey number bounds (in Isabelle/HOL). ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math
• Lean 4.11.0. ~ David Thrane Christiansen. #ITP #Lean4 #FunctionalProgramming

The readings shared in Mastodon on September 1, 2024 are

• Readings shared August 31, 2024. #ITP #Lean4 #IsabelleHOL #Theorema #Coq #Agda #Math #HoTT #Calculemus #PhDThesis
• Modal μ-calculus for free in Agda. ~ Ivan Todorov & Casper Bach Poulsen. #ITP #Agda

The readings shared in Mastodon on August 31, 2024 are

• Readings shared August 30, 2024. #ITP #IsabelleHOL #Agda #Logic #Math #Nix #Haskell #FunctionalProgramming #LogicProgramming
• Proofs of "If x is the supremum of set A, then (∀ y, y < x → ∃ a ∈ A, y < a) in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Unifying model execution and deductive verification with interaction trees in Isabelle/HOL. ~ Simon Foster, Chung-Kil Hur & Jim Woodcock.7# #ITP #IsabelleHOL
• Certification of sorting algorithms using Theorema and Coq. ~ Isabela Drămnesc, Tudor Jebelean & Sorin Stratulat. #ITP #Theorema #Coq
• Investigations in graph-theoretical constructions in Homotopy Type Theory. ~ Jonathan Prieto-Cubides. #PhDThesis #ITP #Agda #HoTT