証明とラムダ計算の一般化／高次化

バエズのセミナーページ http://math.ucr.edu/home/baez/atmcs2008/ からたどれる；

• Vladimir Voevodsky, A very short note on the homotopy lambda calculus, Sept. 27, 2006. (http://math.ucr.edu/home/baez/Voevodsky_note.ps)

very shortすぎてサッパリわからん。何を言いたいかもわからん。

• Yves Guiraud, The three dimensions of proofs, Ann. Pure Appl. Logic 141 (2006), 266-295. (http://arxiv.org/abs/math/0612089)

出だしの印象では意外とわかりやすそう。けっこう長い。