型理論

型理論（かたりろん、英: Type theory）とは、プログラミング・数学・言語学等に現れる型の概念及びそれらが成す型システムを研究対象とする数学・計算機科学の分野である。特定の型システムのことを型理論と呼ぶこともある。