Review of ``Benjamin C. Pierce: Types and programming languages, The MIT Proess, Cambridge, Massachusetts, 2002''

Types were developed in the early part of the 20th century in order to avoid inconsistencies in Frege’s formulation of logic discovered by Russell. They therefore have a strong logical origin, confirmed by the development of Church’s type theory, sometimes called higher-order logic. It contains the simply-typed λ-calculus which is at the core of most modern programming languages. Through the research of other pioneers such as Milner and Martin-Löf, type systems are now understood to be central in the design and analysis of programming languages. They provide the fundamental principles according to which languages are organized. A thorough textbook on type systems in programming languages had been long overdue and Pierce’s book provided exactly that.