Another similar book is Harper's Practical Foundations for Programming Languages[1]. I had the privilege of taking a course[2] about this kind of stuff with Prof. Harper at CMU.

[1]: https://www.amazon.com/Practical-Foundations-Programming-Lan...

[2]: https://www.cs.cmu.edu/~rwh/courses/ppl/

Robert Harper has a great introductory(1) book on the matter

You should have a reasonably complete treatment of what you are looking for by the time you reach the chapter on PCF.

http://www.amazon.com/Practical-Foundations-Programming-Lang...

1: I call it "introductory" because many of the relevant proofs are left as an exercise to the reader. But truthfully, people I've spoken to with a direct influence on the book have mentioned many a time that harper excludes them because he expects you to know them or be able to figure them...