6 ms·

Well, Benjamin Pierce has a 600 page book: http://www.amazon.com/dp/0262162091/ http://www.amazon.com/dp/0262162091/ Followed by a 600 page book: http://www.am

• larsberg 15y ago
  Professor Harper's own book (free! while in draft form), http://www.cs.cmu.edu/~rwh/plbook/book.pdf http://www.cs.cmu.edu/~rwh/plbook/book.pdf , is a better source for understanding the material in this post. But, to be perfectly honest, I'm a systems-focused PL graduate student and have spent quite a bit of time studying this stuff and doubt that I could easily produce a more accessible version of this post. I tried (in the comments block here) and ran on to about two pages before realizing I had only covered the back story on his "trinity" analogy without even getting to this post itself. Someone far smarter than I probably could, but don't feel disappointed if you found this post mathematically challenging even if you normally follow PL theory. It took me a solid cup of coffee and a half an hour to deeply understand what he was saying. Pierce's TAPL primarily covers the type side of this "trinity" and TAPL2 really only has one relevant chapter, covering Dependent Types.
• fogus 15y ago
  Neither of which deal directly with Homotopy Type theory AFAIK.