I am aware that a similar question was asked about the type theory in the principia, but I'm more interested in what the relationship between, say Martin-Lof Type theory and intuitionistic logic is.
-
3What have you uncovered in your research so far? The "Propositions as Types" paper (pdf) may be a good place to start gathering context – Joseph Weissman♦ Sep 29 '15 at 16:42
For Type theory you can see :
Peter Andrews, An Introduction to Mathematical Logic and Type Theory : To Truth Through Proof (1986)
J.Roger Hindley, Basic Simple Type Theory (1997)
Fairouz Kamareddine & Twan Laan, A Modern Perspective on Type Theory (2004)
as well as :
- William Farmer, The Seven Virtues of Simple Type Theory (2008).
On Intuitionistic TT :
Per Martin-Löf, Intuitionistic type theory (1984)
Johan Georg Granström, Treatise on Intuitionistic Type Theory (2011).