nLab Practical Foundations for Programming Languages

The book

lays the foundations of the theory of programming languages in terms of type theory. In over 500 pages, the author formally specifies and step-by-step extends established type systems and reasons about type safety and operational semantics (not so much dependent types and categorical semantics). The book also contains a discussion of logic in type theory and features of variants of the Algol programming language, in particular.

The preview of the second edition (2016) is available as a pdf. A description of the changes is here.