The readings shared in Bluesky on 14 January 2025 are

• Readings shared January 13, 2025. #ITP #Coq #Rocq #HOL4 #CommonLisp #Programming #Math
• An Isabelle/HOL framework for synthetic completeness proofs. ~ Asta Halkjær From. #ITP #IsabelleHOL
• An Isabelle formalization of co-rewrite pairs for non-reachability in term rewriting. ~ Dohan Kim, Teppei Saito, René Thiemann, Akihisa Yamada. #ITP #IsabelleHOL
• Formalizing simultaneous critical pairs for confluence of left-linear rewrite systems. ~ Christina Kirk, Aart Middeldorp. #ITP #IsabelleHOL
• Formalized Burrows-Wheeler transform. ~ Louis Cheung, Alistair Moffat, Christine Rizkallah. #ITP #IsabelleHOL
• Formalizing the one-way to hiding theorem. ~ Katharina Heidler, Dominique Unruh. #ITP #IsabelleHOL
• Further tackling Post correspondence problem and proof generation. ~ Akihiro Omori, Yasuhiko Minamide. #ITP #IsabelleHOL
• The formal theory of monads, univalently. ~ Niels van der Weide. #ITP #Coq #Rocq
• Hell (Haskell shell): Year in review. ~ Chris Done. #Haskell #FunctionalProgramming