Types and programing languages.

*(English)*Zbl 0995.68018
Cambridge, MA: MIT Press. xxi, 623 p. (2002).

The book addresses two main audiences: graduate students and researchers specializing in programming languages and type theory, and graduate students and mature undergraduates from all areas of computer science who want an introduction to key concepts in the theory of programming languages.

A primary aim is coverage of core topics, including basic operational semantics and associated proof techniques, the untyped lambda-calculus, simple type systems, universal and existential polymorphism, type reconstruction, subtyping, bounded quantification, recursive types, and type operators, with shorter discussions of numerous other topics.

A second main goal is pragmatism. The book concentrates on the use of type systems in programming languages, at the expense of some topics (such as denotational semantics) that probably would be included in a more mathematical text on typed lambda-calculi.

Part 1 of the book discusses untyped systems. Basic concepts of abstract syntax, inductive definitions and proofs, inference rules, and operational semantics are introduced first in the setting of a very simple language of numbers and booleans, the repeated for the untyped lambda-calculus.

Part 2 covers the simply typed lambda-calculus and a variety of basic language features such as products, sums, records, variants, references, and exceptions. A preliminary chapter on typed arithmetic expressions provides a gentle introduction to the key idea of type safety. An optional chapter develops a proof of normalization for the simply typed lambda-calculus using Tait’s method.

Part 3 addresses the fundamental mechanism of subtyping: it includes a detailed discussion of metatheory and two extended case studies.

Part 4 covers recursive types, in both the simple iso-recursive and the tricker equi-recursive formulations. The second of the two chapters in this part develops the metatheory of a system with equi-recursive types and subtyping in the mathematical framework of coinduction.

Part 5 takes polymorphism with chapters on ML-style type reconstruction, the more powerful impredicative polymorphism of System \(F\), existential quantification and its connections with abstract data types, and the combination of polymorphism and subtyping in systems with bounded quantification.

Part 6 deals with type operators. One chapter covers basic concepts; the next develops System \(F_w\) and its metatheory; the next combines type operators and bounded quantification to yield System \(F_w\); the final chapter is a closing case study.

The treatment of each language feature discussed in the book follows a common pattern. Motivating examples are first; the formal definitions; then proofs of basic properties such as type safety; the (usually in a separate chapter) a deeper investigation of metatheory, leading to typechecking algorithms and their proofs of soundness, completeness, and termination; and finally (again in a separate chapter) the concrete realization of these algorithms as an Ocalm (Objective Caml) program.

An important source of examples throughout the book is the analysis and design of features for object-oriented programming. Four case study chapters develop different approaches in detail – a simple model of conventional imperative objects and classes, a core calculus based on Java, a more refined account of imperative objects using bounded quantification, and a treatment of objects and classes in the purely functional setting.

A primary aim is coverage of core topics, including basic operational semantics and associated proof techniques, the untyped lambda-calculus, simple type systems, universal and existential polymorphism, type reconstruction, subtyping, bounded quantification, recursive types, and type operators, with shorter discussions of numerous other topics.

A second main goal is pragmatism. The book concentrates on the use of type systems in programming languages, at the expense of some topics (such as denotational semantics) that probably would be included in a more mathematical text on typed lambda-calculi.

Part 1 of the book discusses untyped systems. Basic concepts of abstract syntax, inductive definitions and proofs, inference rules, and operational semantics are introduced first in the setting of a very simple language of numbers and booleans, the repeated for the untyped lambda-calculus.

Part 2 covers the simply typed lambda-calculus and a variety of basic language features such as products, sums, records, variants, references, and exceptions. A preliminary chapter on typed arithmetic expressions provides a gentle introduction to the key idea of type safety. An optional chapter develops a proof of normalization for the simply typed lambda-calculus using Tait’s method.

Part 3 addresses the fundamental mechanism of subtyping: it includes a detailed discussion of metatheory and two extended case studies.

Part 4 covers recursive types, in both the simple iso-recursive and the tricker equi-recursive formulations. The second of the two chapters in this part develops the metatheory of a system with equi-recursive types and subtyping in the mathematical framework of coinduction.

Part 5 takes polymorphism with chapters on ML-style type reconstruction, the more powerful impredicative polymorphism of System \(F\), existential quantification and its connections with abstract data types, and the combination of polymorphism and subtyping in systems with bounded quantification.

Part 6 deals with type operators. One chapter covers basic concepts; the next develops System \(F_w\) and its metatheory; the next combines type operators and bounded quantification to yield System \(F_w\); the final chapter is a closing case study.

The treatment of each language feature discussed in the book follows a common pattern. Motivating examples are first; the formal definitions; then proofs of basic properties such as type safety; the (usually in a separate chapter) a deeper investigation of metatheory, leading to typechecking algorithms and their proofs of soundness, completeness, and termination; and finally (again in a separate chapter) the concrete realization of these algorithms as an Ocalm (Objective Caml) program.

An important source of examples throughout the book is the analysis and design of features for object-oriented programming. Four case study chapters develop different approaches in detail – a simple model of conventional imperative objects and classes, a core calculus based on Java, a more refined account of imperative objects using bounded quantification, and a treatment of objects and classes in the purely functional setting.

Reviewer: G.Bauer (GĂ¶rlitz)

##### MSC:

68N15 | Theory of programming languages |

68-01 | Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science |