26/08/01 10:39:37.45 sQaREFls.net
ホイヨ
”多くの証明支援システムは型理論に基づいている。例えば、Rocq（旧Coq）の基盤となる形式言語は帰納的構成の計算であり、Leanは依存型理論に基づいている。”
(参考)
URLﾘﾝｸ(en.wikipedia.org)
Type_theory
(google訳)
型理論
数理論理学および理論計算機科学において、型理論とは、式や数学的対象をその型によって分類する形式体系の研究である。大まかに言えば、型はプログラミングにおけるデータ型と同様の役割を果たす。つまり、式がどのような種類のものであり、どのように使用できるかを指定する。型理論は、プログラミング言語（型体系）、形式論理、および数学の形式化の研究に用いられる。
数学の基礎として集合論に代わるものとして、いくつかの型理論が提案されてきた。例としては、アロンゾ・チャーチの単純型理論や、ペル・マルティン＝レーフの直観主義型理論などが挙げられる。
多くの証明支援システムは型理論に基づいている。例えば、Rocq（旧Coq）の基盤となる形式言語は帰納的構成の計算であり、Leanは依存型理論に基づいている。