You could try chapter 15 of TFA (http://cs.brown.edu/courses/cs173/2012/book/types.html); http://cs.brown.edu/courses/cs173/2012/book/types.html); otherwise, ye

You could try chapter 15 of TFA (http://cs.brown.edu/courses/cs173/2012/book/types.html); http://cs.brown.edu/courses/cs173/2012/book/types.html); otherwise, yes, TaPL is still very good. An alternative (and rather more difficult) path could be to try working through the Programming Language Foundations volume of Software Foundations (https://softwarefoundations.cis.upenn.edu/plf-current/toc.html https://softwarefoundations.cis.upenn.edu/plf-current/toc.ht...), also by Pierce (and others), which does all its implementation work in Coq (!).