階型理論とも言う

型に関する性質を論ずる形式的体系、またそれによる型付けの規則

数理論理学の一分野

計算機科学よりも歴史が古い

以下より構成される

型付け規則(推論規則)

正しいとわかっている型から推論規則を繰り返し用いて得られる型のみを扱う型理論

ITT nなど

超越的な型の構成も許す型理論

ex. 型上を動く変数の全称束縛を許す型

わからん

参考