型理論の実装
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/07/10 01:05 UTC 版)
さまざまな形式の型理論が、多数の証明支援系の基盤の形式システムとして実装されている。多くがマルティン＝レーフのアイディアに基づいている一方、多くは別の特徴、さらなる公理、もしくは異なる哲学的背景が追加されている。具体的には、NuPRLシステムは、計算型理論（computational type theory）に基づいており、Coqは（余）帰納的構成計算（calculus of (co)inductive constructions）に基づいている。依存型は、ATS、Cayenne、Epigram、Agda、Idrisなどのプログラム言語の設計にも使用される。
※この「型理論の実装」の解説は、「直観主義型理論」の解説の一部です。
「型理論の実装」を含む「直観主義型理論」の記事については、「直観主義型理論」の概要を参照ください。
ウィキペディア小見出し辞書の「型理論の実装」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
- 型理論の実装のページへのリンク
