入学志望の学生さんへ

ここは、プログラム理論（特に論理を使ったプログラム検証、プログラム合成、プログラム変換）、ラムダ計算(全て)、型理論(全て)、数理論理学（特に証明論) の理論的な勉強に打ち込みたい学生に、最適の場所です。私をはじめとして世界で活躍する理論研究者に質問したりアドバイスを受けながら、自分で納得のゆくまでつきつめて勉強することができます。特に、理論研究を深めたい数学、理論計算機科学関係の学生にはとてもよい環境です。また、総合研究大学院大学学生には(社会人学生を除く)全員に国立情報学研究所から月額約10万円が給付されるので経済的にも楽です。意欲ある学生は電子メールでコンタクトしてください。

ここでどういう内容が勉強できるかを知るには次のものを眺めてみてください。

[型理論] 龍田真, 型理論, (近代科学社, 1992.11) 1--82. 私がだいぶ前に書いた型理論の教科書です。本質だけを簡潔に書いてありひとりで読むのは難しいかも知れませんが、このような内容がここで勉強できることが読み取れるでしょう。
[型理論] J.Y. Girard, Y. Lafont and P. Taylor, Proofs and Types (Cambridge University Press, 1989). 型理論の本でもっとも初学者向けの本です。型理論と数理論理(証明論)の両方が書いてあり、このような内容がここで勉強できます。
[数理論理] J.R. Schonfield, Mathematical Logic (Addison-Wesley, 1967). 数理論理の本で初学者でも読み始められる本です。この本のうち証明論に関する部分がここで勉強できます。
[ラムダ計算] 高橋正子「計算論計算可能性とラムダ計算」(近代科学社, 1991). ラムダ計算のよい教科書です。このような内容がここで勉強できます。
[ラムダ計算と型理論] Makoto Tatsuta, Types for Hereditary Permutators, NII Technical Report, NII-2007-010E, 2007, http://research.nii.ac.jp/TechReports/07-010E.html. 私が2007年秋に有名な未解決問題を解いた論文です。学生がこのようなものを目標として最終的にはこれに少しでも近づけるよう勉強できる環境があります。