Type theory and formal proof methods are areas of research that have been gaining much attention in the past years. The first sentence in the Foreword describes the book as “…a gentle, yet profound, introduction to systems of types and their inhabiting lambda-terms,” continuing shortly after with “The book in your hands is focused on the use of types and lambda-terms for the complete formalisation of mathematics.” One can not expect the complete formalisation of mathematics to be accomplished quite that easily, and indeed the book is a long and winding path spanning hundreds of pages and numerous ideas and recent research achievements of a portion of logic whose main focus is on functions.

The classical set-centered approach to the foundations of mathematics, in which a function is a particular kind of relation, and thus a static object, is most likely very familiar to whoever is reading this review. In lambda calculus, however, one treats the notion of function much more dynamically. The theory is much more closely related to logic, as well as to the functional programming paradigm in computer science.

The book introduces (indeed gently) both untyped and typed lambda calculi and proceeds to obtain formalisations of various portions of mathematics, notably, of course, a formalisation of numbers and arithmetic. The authors present the material quite skillfully in the first couple of chapters. They write in a very inviting, interesting, and intriguing manner so that the reader full of set-theoretic prejudices can easily see the inherent beauty of the lambda calculus and appreciate the different perspective it brings to the concept of function — a concept one might have categorized as trivial. That portion of the book can highly be recommended to anybody who wishes to have a better understanding of what lambda calculus is, and what are some of its basic results. The rest of the book delves much deeper and would be of interest to the more specialized reader.

Ittay Weiss is Lecturer of Mathematics at the School of Computing, Information and Mathematical Sciences of the University of the South Pacific in Suva, Fiji.