The readings shared in Bluesky on 4 May 2025 are

• Formalizing resource ownership semantics of spinlocks with the Coq proof assistant. ~ Sebastian Luis S. Ortiz et als. #ITP #Coq #Rocq
• Formalizing reversible computations for synchronous dataflow languages with infinite lists. ~ Sosuke Moriguchi et als. #ITP #Coq #Rocq
• Formal verification of blockchain nonforking in DAG-based BFT consensus with dynamic stake. ~ Alessandro Coglio, Eric McCarthy. #ITP #ACL2
• The minimal megaparsec tutorial. ~ Clément Hurlin. #Haskell #FunctionalProgramming
• Mathematician solves algebra's oldest problem using intriguing new number sequences. ~ University of New South Wales. #Math
• A hyper-Catalan series solution to polynomial equations, and the Geode. ~ N.J. Wildberger, Dean Rubine. #Math
• Entrevista a Jeffrey Ullman (ACM Turing Award). ~ Camilo Chacón Sartori. #Computación