# nLab Practical Foundations for Programming Languages

Related entries

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.

Last revised on May 14, 2021 at 03:38:19. See the history of this page for a list of all contributions to it.