The readings shared in Bluesky on 29 September 2025 are:

• A new proof for soundness of right-forward closures for termination analysis. ~ René Thiemann. #ITP #IsabelleHOL
• Core matrix interpretations for proving termination of term rewrite systems. ~ Ulysse Le Huitouze, René Thiemann. #ITP #IsabelleHOL
• Composition direction of Seymour’s theorem for regular matroids — formally verified. ~ Martin Dvorak et als. #ITP #LeanProver
• Determinism types for functional logic programming. ~ Michael Hanus, Kai-Oliver Prott. #ITP #Rocq
• Cetera: Certified termination with Agda. ~ Dieter Hofbauer, Johannes Waldmann. #ITP #Agda
• Apply the trie: Word search. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang