Quineの存在はKleeneの第2再帰定理から導ける、を型付きラムダ計算で実際に組み立ててみた
Constructing a Quine from Kleene's Second Recursion Theorem
Quineが存在するのはKleeneの第2再帰定理の系にすぎない——ではその構成法を実際に手を動かすとどうなるのか。古典的な計算可能性理論の提示から出発し、関数型プログラミングの視点で定理を述べ直し、Gödelの不完全性定理やTarskiの定義不可能性定理とのつながりにも触れながら、未型付きラムダ計算でChurchエンコーディングによるASTと準クォータを組み立てる。最終的にRocqで形式化し、de Bruijn記法の自己出力項として完成させている。
形式化は機械的な作業とは程遠く、むしろ洞察と創造性の源になり得る（ちなみに、形式検証を単なる転記の作業と見なす一般的な見方が的を外しているのは、まさにこの理由だ）。