This has been my standard desk reference for PL semantics since I started the PhD process five years ago, and I've nearly worn it out.
Be advised that this is definitely not a first book, and that most of the covered topics have simpler introductory treatments elsewhere. This book is mainly a pure semantics work, along the lines of Winskel, Gunter, Tennent, Slonneger, etc. It has no discussion of implementation techniques for any of the covered topics. For that, you're better off with Mitchell's other book, or Sethi or Friedman/Wand/Haynes. Topics covered are: axiomatic, structural operational, and denotational semantics, PCF (including the full abstraction problem), universal algebra, typed lambda calculi and their models (including imperative programs), the category-theoretic approach to domain theory, logical relations, and many chapters on type systems. Several of these topics are covered more extensively elsewhere (domains by Amadio & Curien, types by Pierce), but the... Read more

I started reading this long book in June 2014 and at this writing am well into reading chapter 2, which at huge length introduces Dana Scott's prototype programming language PCF. The first lemmas/theorems/corollaries and their proofs in this book commence in section 2.5.5. At long last, 100 page chapter 2 complete and 90 page chapter 3 started late day of Wed 16Jul14. In at least long sections 3.3 and 3.4 the author puts us in full tilt denotational semantics without ever announcing that to us, but it works out fine anyway. Just an interesting point. I am not too fond of 'algebraic' chap 3, and so will likely not read 31 pg final section 3.7 of that. Did end read of chap 3 after 3.6.4 on Sun 3Aug14 afternoon. Started great chapter 4 on typed lambda calculus the following Monday. Overall, the book still seems to be terrifically interesting and masterfully written.

Typed lambda calculus is the technical home base of the reviewed book, and semantics of programming languages... Read more

0