Reddit reviews Type Theory and Formal Proof: An Introduction
We found 4 Reddit comments about Type Theory and Formal Proof: An Introduction. Here are the top ones, ranked by their Reddit score.
I thought the extreme use of comic sans on this site was pretty amusing. :D
The Lambda Cube is pretty cool - http://www.rbjones.com/rbjpub/logic/cl/tlc001.htm - I'm not sure the page does the best job at explaining it though. The first time I saw a good explanation was in Type Theory and Formal Proof: An Introduction.
Category theory is not easy to get into, and you have to learn quite a bit and use it for stuff in order to retain a decent understanding.
The best book for an introduction I have read is:
Algebra (http://www.amazon.com/Algebra-Chelsea-Publishing-Saunders-Lane/dp/0821816462/ref=sr_1_1?ie=UTF8&qid=1453926037&sr=8-1&keywords=algebra+maclane)
For more advanced stuff, and to secure the understanding better I recommend this book:
Topoi - The Categorical Analysis of Logic (http://www.amazon.com/Topoi-Categorial-Analysis-Logic-Mathematics/dp/0486450260/ref=sr_1_1?ie=UTF8&qid=1453926180&sr=8-1&keywords=topoi)
Both of these books build up from the basics, but a basic understanding of set theory, category theory, and logic is recommended for the second book.
For type theory and lambda calculus I have found the following book to be the best:
Type Theory and Formal Proof - An Introduction (http://www.amazon.com/Type-Theory-Formal-Proof-Introduction/dp/110703650X/ref=sr_1_2?ie=UTF8&qid=1453926270&sr=8-2&keywords=type+theory)
The first half of the book goes over lambda calculus, the fundamentals of type theory and the lambda cube. This is a great introduction because it doesn't go deep into proofs or implementation details.
TAPL can be really hard to grok if it's your first exposure to the notation. I recommend Type Theory and Formal Proof as a first step; the first 100 pages will get you introduced to all of the notation and concepts you need for typing and understanding extensions to the lambda calculus.
TAPL takes over from there with more details on implementing type system features in languages.
Type Theory and Formal Proof covers metatheory all the way up to calculus of constructions, but I think it is at a fairly introductory level and tbh not that insightful from a mathematical perspective. However, it does give a pretty clear exposition of the type checking rules, and is easily converted to an implementation.