From the point of view of its mathematics, logic, and type theory, this book is convincing. It is written with great intensity. Its central topic is the extraction of programs from constructive proofs. It does this by developing a categorical model for the Huet and Coquand calculus of constructions (CC) [1] based on Cartmell’s notion of contextual categories [2]. In a contextual category, the objects are contexts and the arrows are morphisms between contexts. As a result, this book develops an appealing categorical semantics of dependent types, which is linked with the early type theory of Martin-Löf. Although this book is dominated by the development of models for CC, it is still reminiscent of both the content and the style of Martin-Löf’s lectures on intuitionistic type theory [3]. Its apparent indebtedness to Martin-Löf gives this book its strength. In fact, the most interesting part of this book is its formulation of rules for handling “contexts,” where proposition p is an object of type Prop and the type forming construct Proof is applied to p to obtain proofs of p. These rules were motivated by the need to eliminate the ambiguity in CC, which construes propositions as objects of type Prop, and which also construes propositions themselves as types. By contrast, Streicher states, somewhat ambiguously, that “a type will be interpreted as an object in a contextual category and objects will be interpreted as sections of some object and by definition objects and morphisms of a category are disjoint notions” (p. 77). Note that the distinction between Prop and Proof in this book anticipates the formal distinction between the proposition-as-type principle of Curry, Howard, and de Bruijn, and the judgment-as-type principle of Harper, Honsell, and Plotkin [4], which says that the assertion of a judgment in a formal system entails that the judgment has a proof in that system. This distinction is really the significance of the rules of the new CC found in chapter 3.

Structurally, this book consists of an introduction, five chapters, an appendix, references, and an index. Without the introduction, much of what follows would be difficult to understand. The introduction is detailed, occupying 42 pages, and cogently argues its case in the context of CC, Martin-Löf’s type theory, Girard’s polymorphically typed &lgr;-calculus (called system F by Girard in 1972), de Bruijn’s AUTOMATH project, and Scott’s domain theory. A helpful summary of the logical dependencies between the various calculi discussed is also given. This introduction would make an excellent starting point for a graduate (or perhaps even a fourth-year undergraduate) class in programming language theory or software development. Chapter 1 presents a doctrine of constructions based on contextual categories. This chapter requires painstaking care and considerable additional reading in elementary category theory for proper understanding; it is not recommended for the faint-hearted. In chapter2, a sample contextual category based on the category D-Set is given. Chapter 3 is best. It gives the syntactic formulation for CC, and presents a detailed axiomatization of CC in terms of rules for context formation, judgment formation, equality, products of types, and rules for propositions. The disappointment in this chapter is that it assumes rather than proves that the new calculus satisfies properties of strong &bgr;&eegr;-normalization and uniqueness of &bgr;&eegr;-normal forms. A term model for CC is given in chapter 4, and chapter 5 compares the new CC with other approaches.

Although this book is not easy to read due to some poor choices of notation and the author’s penchant for avoiding commas to separate clauses and key phrases in many convoluted sentences, I recommend it highly. It is worth considering for a graduate course in programming language theory or software development theory.