直観主義型理論
出典: フリー百科事典『ウィキペディア(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 外部リンク
Weblioに収録されているすべての辞書から直観主義型理論を検索する場合は、下記のリンクをクリックしてください。
全ての辞書から直観主義型理論 を検索
- 直観主義型理論のページへのリンク