The readings shared in Bluesky on 5 July 2025 are

• The filter game (in Lean 4). ~ Kevin Buzzard. #ITP #LeanProver #Math
• Formal verification of quantum stabiliser codes by stabiliser formalism. ~ Qiuyi Feng. #ITP #CoqProver
• Formal methods at NASA: Past, present, and future. ~ Paul Miner, Natasha Neogi. #FormalMethods #ITP #PVS
• A proof-assisted conversion of signal temporal logic formulas into negative normal form. ~ Danil Berrah, François Pessaux, Alexandre Chapoutot. #ITP #Rocq
• Functorial flattening of the state monad via vector‐space projection (A formally verified collapse model in Lean 4). ~ Jinu Jang. #ITP #LeanProver
• A diagrammatic calculus for a functional model of natural language semantics. ~ Matthieu Pierre Boyer. #Haskell #FunctionalProgramming
• Implementing a type theory with observational equality, using normalisation by evaluation. ~ Matthew Sirman, Meven Lennon-Bertrand, Neel Krishnaswami. #Haskell #FunctionalProgramming
• AI4Research: A survey of artificial intelligence for scientific research. ~ Qiguang Chen et als. #AI
• Curso "Informática (2018-19)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima
• Temas de "Programación funcional" (2018-19). #Haskell #ProgramaciónFuncional
• Ejercicios de programación funcional con Haskell (curso 2018-19). #Haskell #ProgramaciónFuncional
• Exámenes de programación funcional con Haskell (curso 2018-19). #Haskell #ProgramaciónFuncional