3 ms·
Software Foundations (https://softwarefoundations.cis.upenn.edu https://softwarefoundations.cis.upenn.edu) is pretty informal and understandable, what it isn't
by kryptiskt 7y ago
Software Foundations (https://softwarefoundations.cis.upenn.edu https://softwarefoundations.cis.upenn.edu) is pretty informal and understandable, what it isn't is short. But it's a very useful resource.
The best general introduction is probably still Types and Programming Languages: (https://www.cis.upenn.edu/~bcpierce/tapl/index.html https://www.cis.upenn.edu/~bcpierce/tapl/index.html)
It's a great book, but it doesn't get to dependent types.
- ouid 7y agoIt should be mentioned that software foundations is basically a videogame that you can play in your coq interpreter. Short is less relevant than fun, imo.
- polymatter 7y agoI will second that Types and Programming languages is a great book. The next book, https://www.cis.upenn.edu/~bcpierce/attapl/index.html https://www.cis.upenn.edu/~bcpierce/attapl/index.html does get into Dependent Types.
- goodmattg 7y agoI'm currently in Prof. Pierce's class at UPenn! Can confirm this is a great book, and we literally work through the exercises. Taking this class AFTER using Scala in industry has really put a lot into context. It's so easy to start too - download CoqIDE or ProofGeneral and get to it!