型理論
type theory
單純型附きλ計算 (simply-typed lambda calculus)$ \lambda\to
型演算$ \lambda\underline\omega 型無しλ計算
λ-μ 計算
μ 演算子
分岐型理論 (ramified type thory)
依存型理論 (dependent type theory) homotopy 型理論 (homotopy type theory; HoTT)
univalence axiom
higher inductive type
等式型 (identity type。path type)
部分構造型 (substructual type system) pure type system