情報数理領域

情報科学における数理的基礎の領域であり、型理論、数理論理学、プログラム理 論、形式的検証論、アルゴリズム論、広義の離散数学としての符号理論や暗号理 論等について教育研究を行う。

プログラムの性質について正確に論じるためには、プログラム言語の中核部分を 抽象化してその意味を明確にする必要がある。型理論やラムダ計算の理論はその ための理論であり、また、これらの理論は直観主義論理や部分構造論理などの論 理体系とも密接な関係がある。よって、これらの理論に基づいたプログラミング 言語の理論および数理論理学の教育研究を行う。

プログラム理論や形式的検証論は、上記の抽象化された理論を実際のプログラム に適用することを可能にする。計算機プログラムの動作が仕様に沿っているかを 計算機上で検証するためには、それに適したアルゴリズムとデータ構造、さらに 検証全体のための枠組も必要となり、これらを対象とした教育研究を行う。


数学・情報数理学科のページに戻る