Hacker News Reader

Comment by benrbray | Hacker News Reader

Another good reference, that also introduces some PLT notation, is Loh 2001, "Introduction to the Dependently-Typed Lambda Calculus" [1], as well as the textbook by Pierce [2], which has a formally-verified spiritual successor [3].

[1] http://www.cs.ru.nl/~wouters/Publications/Tutorial.pdf [2] https://www.cis.upenn.edu/~bcpierce/tapl/ [3] https://softwarefoundations.cis.upenn.edu/plf-current/index....

View on HN

Types and Programming Languages by Pierce is an amazing book. I'm still far from finishing it, but if anyone is looking for a good introduction to the field, this is it. I consider it to be kind of like the SICP of PL. :)

Edit: Ah, and the Software Foundations books are amazing. I did a little course on formal verification during 2020 and learned a ton. Now every time I work with some kind of type system, I feel frustrated that I can't express everything that I want to in my type system.

Another alternate is "Practical Foundations for Programming Languages" by Bob Harper [1]. It is a bit more broad than TAPL (imo).

[1] https://www.cs.cmu.edu/~rwh/pfpl/

Programming Languages Foundations is an excellent book. Of course it assumes familiarity with Coq (which Logical Foundations covers). Formal proofs about PLs are often boring and tedious to carry out on paper, especially if the property they're stating is clearly obvious, so doing them in an interactive theorem prover is a win-win for checking your work and making the concepts more palatable.

Reply on news.ycombinator.com