Type theory from ground up, first book recomendation

Question

Basically I have a huge problem in finding a decent resource for learning type theory.

I would like you to recommend any kind of resource for learning type theory in mathematical sense.

Also I want to note that I have no prior experience with any kind of type theory(basically all I know about it is that it exists).

So bearing that in mind, where can I go from here?

Answer 1

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

---

You can see also :

• William Farmer, The Seven Virtues of Simple Type Theory (2008).

Answer 2

If you have background in category theory, you might take a look at Categorical Logic and Type Theory by Bart Jacobs.

Like you I had no experience with type theory and I've been told to read it. I'm far from finishing it but so far I'm pretty satisfied.

Edit. Maybe it is worth saying that the book emphasizes the fact that there is not one type theory but numerous ones; basically one for each Grothendieck fibration over nice categories. Just the introduction and the first chapter helped me to understand the differences between simply type theory and dependent type theory for example.