The readings shared in Bluesky on 5 May 2025 are

• Compiling Haskell into Lean: A common abstract syntax for Haskell and interactive theorem provers. ~ Talitha Holcombe. #Haskell #FunctionalProgramming #ITP #LeanProver
• Avaliando a habilidade do ChatGPT de realizar provas de dedução natural em lógica proposicional e lógica de predicados. ~ Francisco Leonardo Batista Martins et als. #LLLms #ChatGPT #Logic
• Typed Lisp, a primer. ~ Musa Al-hassy (2019). #CommonLisp #Haskell