The readings shared in Bluesky on 27 July 2025 are

• Formally verified suffix array construction (in Isabelle/HOL). ~ Louis Cheung, Alistair Moffat, Christine Rizkallah. #FormalVerification #ProofAssistants #IsabelleHOL #Haskell #FunctionalProgramming
• McTT: A verified kernel for a proof assistant. ~ Junyoung Jang et als. #ProofAssistants #Rocq
• Modelling cyclic structures in Agda (Evaluating Agda’s coinduction through modelling graphs). ~ Faizel Mangroe. #ProofAssistant #Agda
• Encoding finite state automata in Agda using coinduction (Evaluating the support for coinduction in Agda). ~ Noky Soekarman. #FormalVerification #ProofAssistant #Agda
• A meta-modal logic for bisimulations (in Isabelle/HOL). ~ Alfredo Burrieza, Fernando Soler-Toscano, Antonio Yuste-Ginel. #ITP #IsabelleHOL
• Solving formal math problems by decomposition and iterative reflection. ~ Yichi Zhou et als. #AI4Math #LLMs #ProofAssistants #LeanProver #Math
• Reseña de «Solving formal math problems by decomposition and iterative reflection». #AI4Math #LLMs #ProofAssistants #LeanProver #Math
• #Exercitium: Problemas de programación con Haskell (febrero de 2019). #Haskell #ProgramaciónFuncional #Matemáticas