型理論
型理論(かたりろん、type theory)
プログラミング言語の型自体とは何かを学ぶには型理論を学ぶ必要がある
ラッセルあたりで単純型理論、分岐型理論が出てきた
最近の型理論はMartin-Löf型理論を基に作られてそう
依存型理論
構成的型理論
ホモトピー理論と型理論を組み合わせて作られたHomotopy Type Theory(HoTT)というものがある
構成されるもの
項(term)
型(type)
判断(judgement)
推論規則
プログラミング言語での定義？
型は値の名前付き集合
値は値集合の要素
→Sets as Types
型理論 インデックス
関連リソース
型理論の資料，リソース
CAPE公開セミナー
関連
帰納的型
可述的
非可述的性
System-F
System U
参考
『型理論Ⅰ』龍田 真