直観主義的型理論
Intuitionistic type theory
https://plato.stanford.edu/entries/type-theory-intuitionistic/
https://en.wikipedia.org/wiki/Intuitionistic_type_theory
http://people.csail.mit.edu/jgross/personal-website/papers/academic-papers-local/Martin-Lof80.pdf
依存型
のある
型付きラムダ計算
？