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