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.
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 :