型理論の歴史
型理論の歴史
キーワード
記述理論
不完全記号 incomplete symbol
文脈の中でのみ意味のある表現
無クラス理論 no-classes theory
置き換え理論
分岐階型理論
1901年
Bertrand RussellがThe Principles of Mathematicsを準備しているときにラッセルのパラドックスを発見
このパラドックスを回避するために型理論が生まれた
The Principles of MathematicsのX章と補遺Bに型理論のアイディアが提示されている
『論理の哲学』 6章に概要が紹介されている
1910年
『Principia Mathematica』
1935年
Kleene-Rosserパラドックス
1967年
Christopher StracheyがAd Hoc多相を提案
Fundamental Concepts in Programming Languagesこれ？
pdf
これは計算機科学側
1971年
Per Martin-Löfが1971年にCurry-Howard同型対応に基づいて型理論を構成した
後にJean-Yves Girardが矛盾していることを発見
Girardの逆説
キーワード
BHK解釈
Solomon Feferman
Klamer Schutte
1972年
Jean-Yves GirardがSystem Fを構成
計算機科学での応用への出発点になる
これは数理論理学側
1974年
John C. ReynoldsがSystem Fと等しい型理論である多相型付きラムダ計算を構成
多相型を扱う
Towards a Theory of Type Structure
pdf
これは計算機科学側
1977年
MLにより多相型の本格的な実用化
Edinburgh LCF: A Mechanized Logic of Computation
Michael J. C. Gordon、Robin Milner、C. P. Wadsworth
1988年
Calculus of Constructionsが発表された
The calculus of constructions pdf
参考
龍田『型理論』 1章
タイプ理論の起源と発展
難しい..mrsekut.icon
この論文はだいぶ詳しいが、mrsekut.iconが理解しきれないのでこのノートにはだいぶ端折りがある
また今度再読しようmrsekut.icon