この方は

国立情報学研究所の先生が型付きラムダ計算についての難問を解決したそうで。未解決問題22問のリストがあって、このリスト中の問題解決は世界初だって。スゲー！

http://d.hatena.ne.jp/siokoshou/20080618#p1

すげー！

問題そのものを解いたのは去年みたいですね。
http://research.nii.ac.jp/TechReports/07-010E.html

まあとりあえず結論的には、
「遺伝的置換子に対する型は存在しない」らしいです。明日テストに出るね。
さっぱりわけワカメです。λ

そんなある日（まあさっきですが）、突然インスピレーションが。
僕のニューロンが微かに反応したので神経回路を探索していたら思い出しました。
USKさんが欲しがってた「型理論」を書いた方だ！
http://d.hatena.ne.jp/uskz/20070829/p1
こんな前のUSKさんの発言を良く覚えていたなっていう。
Googleからの怪しげなrefererは多分わたくしです。

型理論に興味あるけれどラムダ計算に興味あるけれど
とりあえず僕は数理論理の基礎をもっと学ばないといけない。
しかし完全に中断してしまっている。。。
この本を読み終えると次に待っている本には型付ラムダ計算がちょっと出てくるっぽい。