Books on programming language semantics
It all depends how deep you want to go, and how much you already know. For a beginner Winksel's book is really nice, but yes, it's not introducing you to the state of the art in semantics as it was written about 20 years ago. Nevertheless it's still a good first introduction to the subject. It might also be worthwhile pointing out that T. Nipkow has formalised a substantial chunk of Winskel's book in Isabelle/HOL, see here. So if you want to learn using interactive proof assistants together with understanding the semantics of programming languages, you have a lot of coherent material to draw on.

Other books that are more advanced are:


Gunter, Semantics of Programming Languages, a more advanced book focussing on denotational semantics, an approach to semantics, which hasn't lived up to expectations. Focusses on purely functional lanugages and ignores concurrency. This is the book that I taught myself semantics from as an undergraduate, and in retrospect I wish I had used Winksel's book instead. Gunter is not an easy read for a beginner.
Domains and lambda-calculi by Amadio and Curien. Another book coming written more in the domain-theoretic tradition, although it discusses process calculi.
John Mitchell's books which have already been mentioned above. They are also mostly about sequential computation.


Books like Pierce's TAPL are very nice, but focus narrowly on one aspect of programming languages, namely types, as important as that is. I would not recommend it as a first introduction to the general area of programming languages, but it is mandatory to read for anyone who wants to learn about types.

Truth be told, I think there's currently no up-to-date introductory book on language semantics that reflects the substantial progress the last decade has seen, with its decisive shift away from denotational methods and sequential computation to concurrency (process calculi and game semantics), axiomatics semantics and the use of interactive proof assistants in verification. 

Update 22. April 2014: Tobias Nipkow and Gerwin Klein have published a new book


Concrete Semantics


which can be seen as 'Winskel in Isabelle/HOL'. It's an introduction to the
semantics of programming languages (primarily operational and
axiomatic) but unlike previous pen-and-paper-based approaches, this
book expresses all its mathematics in Isabelle/HOL. In other words,
it's at the same time a book about theorem proving.

The book is brand new so I have not used for teaching, but it looks really suitable
as an introduction that is pitched at a lower level than Software Foundations
by 
Pierce et al.