The readings shared in Bluesky on 17 April 2025 are

• Formalization of Fraïssé limits in Lean. ~ Gabin Kolly. #ITP #LeanProver #Math
• A readable and computable formalization of the Streamlet consensus protocol. ~ Mauro Jaskelioff, Orestis Melkonian, James Chapman. #ITP #Agda
• The Haskell Unfolder Episode 42: Logic programming with typedKanren. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• #Exercitium: Emparejamiento de árboles. #Haskell #ProgramaciónFuncional
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Si u ⊆ v, entonces f⁻¹[u] ⊆ f⁻¹[v]​". #LeanProver #IsabelleHOL #Math