Martin-Löfの直観主義型理論
直観主義的型理論(ちょっかんしゅぎてきかたりろん、Intuinistic type theory)
Per Martin-Löf
によって開発された
型理論
$ \mathbf{ITT}_n
→
Martin-Löf型理論
直観主義
直観主義論理
カリー＝ハワード対応
ラムダ計算
BHK解釈
帰納的、演繹的
BHK解釈
構成的型理論
依存型理論
直観主義型理論 - Wikipedia
『Intuitionistic Type Theory』Stanford Encyclopedia of Philosophy
関連
型付きラムダ計算
#型理論