「型推論」特別講義

YouTube再生リスト 「型推論」特別講義 (プログラミング言語の基礎理論シリーズ） にまとめられたビデオ講義．

ML系多相型プログラミング言語（Standard ML、OCaml、SML# など）の型推論 の本質、理論的基礎、アルゴリズムの詳細とその性質に関する講義です。大学 院レベルの理論的な内容を含みますが、型理論の専門知識を持たない学部生で も理解できるself-containedなものとなるように構成します。

教科書は、大堀 淳著、新装版 プログラミング言語の基礎理論、共立出版 です。この中で，

• 第１章 プログラミング言語のモデル
  • 1.3.1 形式言語の帰納的な定義
  • 1.3.2 言語に対する再帰的な関数定義と文法の曖昧さ（一部）
  • 1.4.1 型無しラムダ計算の定義
• 第４章 型推論システム（全般）
• 第5章 多相型言語のモデル （以下の部分）
• 5.6.5 MLの型推論システム

をカバーし、さらにそれを超えるMLの型推論の最先端の内容を含みます。

MLの型推論は、種々の解説や教科書などで「式に対して主要な型を推論する」 等と説明されよく理解されていると思われるかもしれませんが、それらの説明 には技術的に曖昧・不正確な点が含まれ、また、その理論的基礎の詳細も殆ど 説明されていないのが現状です。この現状を踏まえ、本講義では、型推論が基 礎とする理論、既存のアルゴリズムの分析、さらに、最先端の理論に基づくML の型推論アルゴリズムの提示を通じて、MLの型推論の本質ならびに型推論アル ゴリズムの詳細を正確に理解できる講義の提供を目指します。