The readings shared in Bluesky on 14 November 2025 are:

• An introduction to formal real analysis (Lecture 18: Rearrangements). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in Rocq. ~ Nicolas Chappe et als. #ITP #Rocq
• A practical formalization of monadic equational reasoning in dependent-type theory. ~ Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. #ITP #CoqProver
• Towards type-directed compiler calculation. ~ Wouter Swierstra. #ITP #Agda
• Binary search—think positive. ~ Alexander Dinges, Ralf Hinze. #ITP #Agda
• Checking equivalence in a non-strict language. ~ John Charles Kolesar, Ruzica Piskac, William Triest Hallahan.7#supplementary-materials #Haskell #FunctionalProgramming
• Automatically testing console I/O behavior of student submissions in Haskell. ~ Oliver Westphal, Janis Voigtländer. #Haskell #FunctionalProgramming
• Parallel dual-numbers reverse AD. ~ Tom J. Smeding, Matthijs I.L. Vákár. #Haskell #FunctionalProgramming
• Domain-specific tensor languages. ~ Jean-Philippe Bernardy, Patrik Jansson. #Haskell #FunctionalProgramming
• Turner, Bird, Eratosthenes: An eternal burning thread. ~ Jeremy Gibbons. #Haskell #FunctionalProgramming
• How much is in a square? Calculating functional programs with squares. ~ Jose Nuno Oliveira. #Haskell #FunctionalProgramming
• Experiences of early assessment to teach functional programming. ~ Peter Chapman. #Haskell #FunctionalProgramming
• You could have invented Fenwick trees. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• Patterns and paradoxes: The logic of pattern synonyms. ~ Koz Ross. #Haskell #FunctionalProgramming
• The Haskell Unfolder Episode 49: Shrinking. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• The Haskell Unfolder Episode 50: Singletons. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• The Haskell Unfolder Episode 51: Typed servers using sop-core. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• Tail recursion modulo context: An equational approach. ~ Daan Leijen, Anton Felix Lorenzen. #OCaml #FunctionalProgramming
• How we achieved an IMO medal, one year before any other AI system. ~ Tom Zahavy. #AI #Math #ITP #LeanProver #AlphaProof
• Olympiad-level formal mathematical reasoning with reinforcement learning. ~ Thomas Hubert et als. #AI #Math
• Reseña de «Olympiad-level formal mathematical reasoning with reinforcement learning». #AI #Math #ITP #LeanProver #AlphaProof
• #Exercitium: Cuantificadores sobre listas. #Haskell #ProgramaciónFuncional