The readings shared in Bluesky on 17 August 2025 are

• Beyond booleans. ~ Dan Abramov. #ITP #LeanProver
• Counterpart-based quantified temporal logics. ~ Fabio Gadducci, Andrea Laretto, Davide Trotta. #ITP #Agda
• Type soundness of functional languages with subtyping in Lang-n-Prove. ~ Matteo Cimini, Joan Montas. #ITP #Abella
• Invertible syntax without the tuples (Functional Pearl). ~ Mathieu Boespflug, Arnaud Spiwack. #Haskell #FunctionalProgramming
• Understanding Fermat's Last Theorem's proofs. ~ Alex Qiu et als. #Math