The readings shared in Bluesky on 15 October 2025 are:

• Rely-guarantee verification of queue locks with proof support in Isabelle/HOL. ~ Robert J. Colvin, Scott Heiner, Peter Höfner, Roger C. Su. #ITP #IsabelleHOL
• Formal verification of COO to CSR sparse matrix conversion. ~ Andrew W. Appel. #ITP #CoqProver
• Mechanizing Olver's error arithmetic. ~ Max Fan, Ariel E. Kellison and Samuel D. Pollard. #ITP #Rocq
• Formal verification of Graham’s scan algorithm. ~ Yingjun Lan, Yuxuan Sun. #ITP #Rocq
• Separation logics for probability, concurrency, and security. ~ Kwing Hei Li. #ITP #Rocq
• McTT: A verified kernel for a proof assistant. ~ Junyoung Jang, Antoine Gaulin, Jason Z. S. Hu, Brigitte Pientka. #ITP #Rocq #OCaml #FunctionalProgramming
• Formalizando um teorema de classificação para álgebras de Lie solúveis de baixa dimensão em Lean. ~ Gustavo Infanti, Viviana del Barco, Exequiel Rivas, Paul Schwahn. #ITP #LeanProver #Math
• Verifying the functional correctness of Braun trees with LiquidHaskell. ~ Felipe de León, Alberto Pardo, Marcos Viera. #Haskell #FunctionalProgramming #LiquidHaskell
• How much is in a square? Calculating functional programs with squares. ~ Jose Nuno Oliveira. #Haskell #FunctionalProgramming
• Arrows to arrows, categories to queries. ~ Sandy Maguire. #Haskell #FunctionalProgramming
• DRIFT: Decompose, retrieve, illustrate, then formalize theorems. ~ Meiru Zhang, Philipp Borchert, Milan Gritta, Gerasimos Lampouras. #AI #Math #LLMs #ITP #LeanProver
• Books to recommend to maths students. ~ Katie Steckles. #Math