A Quine Built from Kleene's Second Recursion Theorem, Formalized in Rocq

Constructing a Quine from Kleene's Second Recursion Theorem

Kleene's second recursion theorem guarantees that quines exist, but how hard is it to actually build one from the construction? The author walks through a functional-programming presentation of the theorem, then implements it in the untyped lambda calculus using Church encodings for syntax trees and a quasi-quoter, and verifies the whole thing in Rocq. Along the way, typed and untyped views connect the theorem to Gödel's diagonal lemma and Tarski's undefinability theorem.