Type Theory quick question
post by Faustus2 · 2017-07-26T19:57:02.877Z · LW · GW · Legacy · 6 commentsContents
6 comments
Just 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.
comment by justinpombrio · 2017-07-26T22:31:46.835Z · LW(p) · GW(p)
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)
Replies from: Faustus2, gwillen↑ comment by Faustus2 · 2017-07-27T19:16:02.283Z · LW(p) · GW(p)
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
Replies from: justinpombrio↑ comment by justinpombrio · 2017-07-27T22:14:57.041Z · LW(p) · GW(p)
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.
comment by MrMind · 2017-07-27T12:31:02.347Z · LW(p) · GW(p)
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.