LESSWRONG
LW

Personal Blog

0

Type Theory quick question

by Faustus2
26th Jul 2017
1 min read
6

0

Personal Blog

0

Type Theory quick question
4justinpombrio
1Faustus2
0justinpombrio
1gwillen
3MrMind
0Manfred
New Comment
6 comments, sorted by
top scoring
Click to highlight new comments since: Today at 12:57 PM
[-]justinpombrio8y40

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)

Reply
[-]Faustus28y10

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

Reply
[-]justinpombrio8y00

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.

Reply
[-]gwillen8y10

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

Reply
[-]MrMind8y30

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.

Reply
[-]Manfred8y00

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

Reply
Moderation Log
More from Faustus2
View more
Curated and popular this week
6Comments

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.