I agree, but Concrete Semantics and the other 2 equivalent references are a general introduction to everything.

Yes, they use theorem provers, but proofs are optional and not required to follow the material. And they do cover those topics you mention.