It gets pretty math-heavy at times, at least in the beginning (you can probably skip the first chapter if it's too rough), but ultimately the book is about programming language design and different ways of designing and evaluating typed (or un(i)typed) languages. It also looks at a large number of important languages including PCF, Typed/Untyped Lambda Calculus, System F, Gödel's T and ALGOL (the last of which is interesting because it uses what we now call the IO Monad).
I'm taking the class (15-312) right now, and as homework we typically implement an interpreter for some language using SML (OCaml would likely work fine for the general use case), and then prove a few things about the language. Our languages rely on our Abstract Binding Tree (ABT) infrastructure that we developed early on in the course. You can find the course page at http://www.cs.cmu.edu/~rjsimmon/15312-s14/index.html if you want to check out what we're working on.
PFfPL is a great book. It manages to present many seemingly different language features in a surprisingly unified way.
It's very opinionated at times (usually against anything "dynamic", eg. typing and binding ;) ) but I think it's worth it for the clarity that it allows. Of course, Bob Harper has the clout to back up those opinions!
I try to take a break from proving progress and preservation by reading hackernews and of course I find someone talking about 15-312 :/ Either way, I would agree with you in recommending the text.
I've been wanting to read that for a while. Another candidate is Pierce's "Types and Programming Languages". Has anybody by any chance read both an can compare them?
TAPL isn't Coq-focused. Pierce and his collaborators have another book available online, Software Foundations, which is written as a Coq literate program:
http://www.cis.upenn.edu/~bcpierce/sf/index.html
http://www.cs.cmu.edu/~rwh/plbook/book.pdf
It gets pretty math-heavy at times, at least in the beginning (you can probably skip the first chapter if it's too rough), but ultimately the book is about programming language design and different ways of designing and evaluating typed (or un(i)typed) languages. It also looks at a large number of important languages including PCF, Typed/Untyped Lambda Calculus, System F, Gödel's T and ALGOL (the last of which is interesting because it uses what we now call the IO Monad).
I'm taking the class (15-312) right now, and as homework we typically implement an interpreter for some language using SML (OCaml would likely work fine for the general use case), and then prove a few things about the language. Our languages rely on our Abstract Binding Tree (ABT) infrastructure that we developed early on in the course. You can find the course page at http://www.cs.cmu.edu/~rjsimmon/15312-s14/index.html if you want to check out what we're working on.