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 (@LawrPaulson@mathstodon.xyz). #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