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