3 ms·
Another good reference, that also introduces some PLT notation, is Loh 2001, "Introduction to the Dependently-Typed Lambda Calculus" [1], as well as the textboo
by benrbray 5y ago
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 http://www.cs.ru.nl/~wouters/Publications/Tutorial.pdf
[2] https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/
[3] https://softwarefoundations.cis.upenn.edu/plf-current/index.html https://softwarefoundations.cis.upenn.edu/plf-current/index....
- ashton314 5y agoTypes 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.
- shadowfox 5y agoAnother 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/ https://www.cs.cmu.edu/~rwh/pfpl/
- siraben 5y agoProgramming 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.