Programming Languages Foundations is an excellent book. Of course it assumes familiarity with Coq (which Logical Foundations covers). Formal proofs about PLs ar

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.