The readings shared in Bluesky on 13 October 2025 are:

• PVS formalization of proofs of the infinitude of primes. ~ Bruno Berto de Oliveira Ribeiro. #ITP #PVS #Math
• Certified decision procedures for width-independent bitvector predicates. ~ Siddharth Bhat, Léo Stefanesco, Chris Hughes, Tobias Grosser. #ITP #LeanProver
• Interactive theorem provers for proof education. ~ Romina Mahinpei, Manoel Horta Ribeiro, Mae Milano. #ITP #CoqProver #Teaching
• Pyrosome: Verified compilation for modular metatheory. ~ Dustin Jamner, Gabriel Kammer, Ritam Nag, Adam Chlipala. #ITP #CoqProver
• Incremental certified programming. ~ Tomás Díaz, Kenji Maillard, Nicolas Tabareau, Éric Tanter. #ITP #Rocq
• Proof repair across quotient type equivalences. ~ Cosmo Viola, Max Fan, Talia Ringer. #ITP #Rocq
• Don’t call us, we’ll call you (Towards mixed-initiative interactive proof assistants for programming language theory). ~ Jan Liam Verter, Tomas Petricek. #ITP #Teaching
• Synthesizing implication lemmas for interactive theorem proving. ~ Ana Brendel, Aishwarya Sivaraman, Todd Millstein. #ITP #Rocq
• Deriving an Erlang interpreter from a mechanised formal semantics of core Erlang. ~ Gergő Lajos Turán, Arsenii Fomin, Péter Bereczky, Dániel Horpácsi, Simon Thompson. #ITP #Agda #FunctionalProgramming #Erlang
• Checking a denotational semantics of Scheme in Agda. ~ Peter D. Mosses. #ITP #Agda
• Mechanised proofs of atom exhaustion in Erlang. ~ Arsenii Fomin, Péter Bereczky, Dániel Horpácsi, Gergő Lajos Turán. #ITP #Rocq
• Formalizing the zigzag construction of path spaces of pushouts. ~ Vojtěch Štěpančík. #ITP #Agda
• Unification modulo isomorphisms between dependent types for type-based library search. ~ Satoshi Takimoto, Sosuke Moriguchi, Takuo Watanabe. #Haskell #FunctionalProgramming
• Representing data structures with invariants in Haskell: The cases of BST and AVL. ~ Nicolas Rodriguez, Alberto Pardo, Marcos Viera. #Haskell #FunctionalProgramming
• A formalization of opaque definitions for a dependent type theory. ~ Nils Anders Danielsson, Eve Geng. #ITP #Agda #FunctionalProgramming
• The conatural numbers form an exponential commutative semiring. ~ Szumi Xie, Viktor Bense. #ITP #Agda #FunctionalProgramming
• A tale of two lambdas: A haskeller’s journey into OCaml. ~ Richard A. Eisenberg. #Haskell #OCaml #FunctionalProgramming
• A Clash course in solving Sudoku (Functional pearl). ~ Gergő Érdi. #Haskell #FunctionalProgramming
• The calculated typer (Functional pearl). ~ Zac Garby, Patrick Bahr, Graham Hutton. #Haskell #FunctionalProgramming
• Plinth: A plugin-powered language built on Haskell. ~ Ziyang Liu, Kenneth MacKenzie, Roman Kireev, Michael Peyton Jones, Philip Wadler, Manuel Chakravarty. #Haskell #FunctionalProgramming
• Rebound: Efficient, expressive, and well-scoped binding. ~ Noé De Santo, Stephanie Weirich. #Haskell #FunctionalProgramming
• Total type classes. ~ Robert Weingart, Nicolas Wu. #Haskell #FunctionalProgramming
• Automatic C bindings generation for Haskell. ~ Travis Cardwell, Sam Derbyshire, Edsko de Vries, Dominik Schrempf. #Haskell #FunctionalProgramming
• Lightweight testing of persistent amortized time complexity in the credit monad. ~ Anton Lorenzen. #Haskell #FunctionalProgramming
• Freer arrows and why you need them in Haskell. ~ Grant VanDomelen, Gan Shen, Lindsey Kuper, Yao Li. #Haskell #FunctionalProgramming
• Staging automatic differentiation with fusion. ~ Samuel Klumpers, Tom Schrijvers. #Haskell #FunctionalProgramming
• An empirical evaluation of property-based testing in Python. ~ Savitha Ravi, Michael Coblenz. #Python #Programming