Another good one is: * Concrete Semantics by Nipkow and Klein http://concrete-semantics.org/ http://concrete-semantics.org/, which is also an introduction to t

Another good one is: * Concrete Semantics by Nipkow and Klein http://concrete-semantics.org/ http://concrete-semantics.org/, which is also an introduction to the Isabelle/HOL proof assistant and formalizes all of the PL content in Isabelle There's also: * Semantics with Applications: An Appetizer by Nielson and Nielson https://www.springer.com/gp/book/9781846286919 https://www.springer.com/gp/book/9781846286919, apparently a newer edition of an older book I liked and which used to be available as a free PDF, but the link from my browser history is now broken