その他の記事

• Mario Carneiro による Lean の型理論

• Lean 公式カーネル：https://github.com/leanprover/lean4/tree/master/src/kernel

• lean4lean、Lean 4 による Lean カーネルの再実装

• lean4export、Lean 4 環境のオフィシャル・推奨エクスポータ

• lean4checker

• Peter Dybjer による Lean で実装される帰納型に関するオリジナルの記述：P. Dybjer. Inductive families. Formal aspects of computing, 6(4):440–465, 1994.

• Conor McBride と James McKinna の論文 I am not a number: I am a free variable は束縛・自由変数への locally nameless なアプローチを記述しています。

• 帰納型における positive ではない出現に関する情報、Counterexamples in Type Systems: https://counterexamples.org/strict-positivity.html?highlight=posi#positivity-strict-and-otherwise

• Freek Wiedijk. Pollack-inconsistency. Electronic Notes in Theoretical Computer Science, 285:85–100, 2012