Lӧb's Theorem: A functional pearl of dependently typed quining A write-up of https://github.com/JasonGross/lob The Current Draft (.pdf) The Current Draft (.pdf, preprint) The Current Draft (.html) The construction of a quine (.html) An anonymized README describing a bit of the code structure in the repo.