型理論、依存型理論を学習する
型理論
、
依存型理論
を学ぶには
Programming in Martin-Löf’s Type Theory
Martin-Löf型理論(MTT)
Type-Driven Development with Idris
A Tutorial Implementation of a Dependently Typed Lambda Calculus
『Homotopy Type Theory Univalent Foundations of Mathematics』
P
直観的型理論(intensional type theory)
intensional type theory in nLab
『Types and Programming Languages』(TaPL)
関連しそうなもの
『Constructive Mathematics』
type theory in nLab
日本語文献
『型システム入門』
CAPE公開セミナー
大堀淳の計算機科学チャネル - YouTube
Tatsuta Entrance
計算機科学のための圏論の基礎の基礎
自分のメモページ:
『計算機科学のための 圏論の基礎の基礎』
ホモトピー型理論
Homotopy Type Theoryの参考文献
『Homotopy Type Theory Univalent Foundations of Mathematics』
『Introduction to Homotopy Type Theory』
参考
型理論の資料，リソース - パンの木を植えて
Good introductory book to type theory? - MathOverflow