The book is an introduction to one of the dialects of type theory. All type theories are grounded in logic. The promise of simple type theory is that it can be understood and handled much easier than other versions of type theory, for example, dependent type theory or homotopy type theory.

The author presents the basic concepts of simple type theory and justifies why this logic approach was selected over other possible logic and mathematical formal languages, for example, set theory or first-order logic. The book is based on Alonzo type theory, developed by Alonzo Church. The thesis of the book is that this type of theory can be managed easily--or with at least reasonable effort by practicing mathematicians and designers of computer programs.

Chapter 3 overviews the basic concept of mathematics and its relationships and representations in type theory. Chapter 4 describes the syntax of Alonzo type theory, the notational conventions, and the compact and formal notation of this logic language. It is an important chapter because the other chapters are incomprehensible without knowledge of syntactical rules. Chapter 5 displays the semantics of the Alonzo type theory on a model-theoretic basis. Chapters 6 and 7 enhance the notational conventions, including the logical quantifiers and then the rewriting rules to expand the expressions and formulas using substitutions. Chapter 8 showcases the proof systems of Alonzo type theory, or more accurately the customization of proof systems in logics for this type theory.

From a practical view, chapter 9 is one of the most important chapters since it demonstrates how the theories, their theorems, and their proofs can be used in an environment that requires formal verification and validation of mathematical theories and problems. Chapter 10 contains the formalization of sequences in Alonzo type theory that are frequent actors in algorithms. Chapter 11 relies on the two previous chapters to display the theory development, that is, how definitions can be made and how theorems can be stated and proved in Alonzo type theory by practicing mathematicians. Chapter 12 is a kind of case study from a mathematician’s point of view; namely, the foundations of real numbers and calculus are presented. Chapter 13 is about morphisms, which are called interpretations of logic models in other model-theoretic and logic approaches. Naturally, the chapter on morphisms describes the interpretation of models in the context of Alonzo type theory. Chapter 14 discusses the augmentation of the core Alonzo type theory, for example, the extension of types by sorts. The concluding chapter (15) surveys the possible software support for Alonzo type theory since simple type theory has LaTeX support to write papers; however, there is no direct software or interpreter that can assist with writing theories and formal checks. The dependent type theories have the Agda and Irdis programming languages; there is a Coq proof system and operationalizable language for mathematics.

Anyway, the book is a good summary and introduction to type theory; however, the dearth of software and programming support does not make it feasible for teaching when alternative (and even more complex) type theories have automated support for creating, verifying, and validating mathematical and computer science theories that can be formal models of algorithms or mathematical theorems. To use Alonzo simple type theory, the user should understand the syntax and underlying semantics of the theory, which are slightly different from other concurrent approaches; it requires a deep dive into the details in order to employ them fluently. The book is a good scientific book, and it could even be used as a textbook; that being said, it will work best at colleges and universities where there exists a strong research and education community specializing in simple type theory and Alonzo Church’s approach.