2. Agenda はじめに Part I : 「型の理論」をふりかえる Part II : Curry-Howard対応について Part III: Coq入門 3. はじめに 現在、HoTT(Homotopy Type Theory)と呼 ばれる新しい型の理論とそれを基礎付ける Univalent Theoryと呼ばれる新しい数学理論 が、熱い関心を集めている。 Univalent Theoryは、数学者のVladimir Voevodskyが、論理学者Per Martin-Löfの型 の理論を「再発見」したことに始まる。 この新しい分野は、21世紀の数学とコンピュ ータサイエンスの双方に、大きな影響を与え ていくだろう。
