The readings shared in Bluesky on 3 July 2025 are

• LeanLTL: A unifying framework for linear temporal logics in Lean. ~ Eric Vin, Kyle A. Miller, Daniel J. Fremont. #ITP #LeanProver
• Verifying Datalog reasoning with Lean. ~ Johannes Tantow, Lukas Gerlach, Stephan Mennicke, Markus Krötzsch. #ITP #LeanProver
• Formalising inductive and coinductive containers. ~ Stefania Damato, Thorsten Altenkirch, Axel Ljungström. #ITP #Agda