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