# Type Theory quick question

post by Faustus2 · 2017-07-26T19:57:02.877Z · score: 0 (0 votes) · LW · GW · Legacy · 6 commentsJust a quick question, does anybody know or recommend any resources to learn type theory? I do a lot of independent study in my spare time and would be appreciative if anyone has any insight into how to approach this topic from the self-study angle.

## 6 comments

Comments sorted by top scores.

What is your goal? Type theory is at the intersection of programming languages and logic. If you care about programming languages and type systems, read TAPL:

https://www.cis.upenn.edu/~bcpierce/tapl/

If you care about type theory purely as a logic, I don't have an obvious recommendation, but could point you at some material.

(Programming Languages researcher)

The goal is mainly to understand its relation to proof assistants, I have experience with it before as a purely logical study but i haven't tried to see it in this new context for myself. This book looks excellent though, thank you for your recommendation

Ah, then you'll want to read about the [https://hal.inria.fr/inria-00076024/document](Calculus of Constructions):

Yeah, TAPL is *the* book on type systems. I'm not aware of competition.

Seconding TAPL, it was the textbook for the type theory course I took in college, it is topnotch.

It reeeeeeally depends on your background. You can come at TT from many different directions: logic, programming, category theory, algebraic topology... the good news is that the contemporary view is that those are all facets of the same thing, a sort of generalized Church-Turing thesis.

The HoTT book is pretty readable, but I'm not in a position to evaluate its actual goodness.