What it the relationship between Type theory and logic?

Question

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.

Answer 1

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