直観主義型理論
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2023/06/08 13:42 UTC 版)
直観主義型理論（ちょっかんしゅぎかたりろん、英: intuitionistic type theory）とは、数学の代替基盤を目指して論理学・哲学者のペール・マルティン＝レーフによって開発された型理論を言う。構成的型理論（constructive type theory）、またはマルティン＝レーフの型理論（Martin-Löf's type theory）とも呼ばれる。1972年に最初のバージョンが発表された。直観主義型理論には複数のバージョンがある。
- ^ Allen, S.F.; Bickford, M.; Constable, R.L.; Eaton, R.; Kreitz, C.; Lorigo, L.; Moran, E. (2006). “Innovations in computational type theory using Nuprl”. Journal of Applied Logic 4 (4): 428–469. doi:10.1016/j.jal.2005.10.005.
- ^ Norell, Ulf (2009). Dependently Typed Programming in Agda. TLDI '09. New York, NY, USA: ACM. 1–2. doi:10.1145/1481861.1481862. ISBN 9781605584201
- ^ Brady, Edwin (2013). “Idris, a general-purpose dependently typed programming language: Design and implementation”. Journal of Functional Programming 23 (5): 552–593. doi:10.1017/S095679681300018X. ISSN 0956-7968.
[続きの解説]
「直観主義型理論」の続きの解説一覧
- 1 直観主義型理論とは
- 2 直観主義型理論の概要
- 3 型理論の実装
- 4 参考文献
- 5 外部リンク
- 直観主義型理論のページへのリンク
