型理論の歴史

キーワード

不完全記号 incomplete symbol

文脈の中でのみ意味のある表現

無クラス理論 no-classes theory

1901年

Bertrand RussellがThe Principles of Mathematicsを準備しているときにラッセルのパラドックスを発見

このパラドックスを回避するために型理論が生まれた

The Principles of MathematicsのX章と補遺Bに型理論のアイディアが提示されている

『論理の哲学』 6章に概要が紹介されている

1910年

1935年

1967年

Christopher StracheyがAd Hoc多相を提案

Fundamental Concepts in Programming Languagesこれ？

これは計算機科学側

1971年

Per Martin-Löfが1971年にCurry-Howard同型対応に基づいて型理論を構成した

後にJean-Yves Girardが矛盾していることを発見

キーワード

1972年

Jean-Yves GirardがSystem Fを構成

計算機科学での応用への出発点になる

これは数理論理学側

1974年

John C. ReynoldsがSystem Fと等しい型理論である多相型付きラムダ計算を構成

多相型を扱う

これは計算機科学側

1977年

MLにより多相型の本格的な実用化

Michael J. C. Gordon、Robin Milner、C. P. Wadsworth

1988年

Calculus of Constructionsが発表された

The calculus of constructions pdf

参考

龍田『型理論』 1章

難しい..

この論文はだいぶ詳しいが、が理解しきれないのでこのノートにはだいぶ端折りがある

また今度再読しよう