New: Type Theory

Author: wdv4758h

programming-language/theory-and-concepts/type-theory.rst

@@ -0,0 +1,66 @@
+========================================
+Type Theory
+========================================
+
+
+.. contents:: 目錄
+
+
+簡單介紹
+========================================
+
+歷史
+========================================
+
+1900 ~ 1927
+-----------------------------------
+
+羅素悖論（理髮師悖論）（Origin of Russell's theory of types）
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+
+重要人物：
+
+* Gottlob Frege
+* Bertrand Russell
+* Willard Quine
+
+
+理論：
+
+1. the zigzag theory
+2. theory of limitation of size,
+3. the no-class theory (1905–1906)
+4. readopting the theory of types (1908)
+
+
+1908 - "ramified" theory of types
++++++++++++++++++++++++++++++++++
+
+重要人物：
+
+* Stephen Kleene
+
+
+1971 ~ 1984 - Martin-Löf's Intuitionistic Type Theory
++++++++++++++++++++++++++++++++++++++++++++++++++++++
+
+1991 - Barendregt's lambda cube
++++++++++++++++++++++++++++++++
+
+
+
+Alonzo Church - λ calculus
+========================================
+
+Per Martin-Löf - Intuitionistic Type Theory
+===========================================
+
+
+參考
+========================================
+
+* `Wikipedia - Type Theory <https://en.wikipedia.org/wiki/Type_theory>`_
+* `Wikipedia - History of type theory <https://en.wikipedia.org/wiki/History_of_type_theory>`_
+* `The collected works of Per Martin-Löf <https://github.com/michaelt/martin-lof>`_
+* `Stanford Encyclopedia of Philosophy - Intuitionistic Type Theory <http://plato.stanford.edu/entries/type-theory-intuitionistic/>`_
+* `Stanford Encyclopedia of Philosophy - Russell's Paradox <http://plato.stanford.edu/entries/russell-paradox/>`_