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.