You are here

Type Theory and Formal Proof: An Introduction

Rob Nederpelt and Herman Geuvers
Cambridge University Press
Publication Date: 
Number of Pages: 
[Reviewed by
Ittay Weiss
, on

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.

Greek alphabet
1. Untyped lambda calculus
2. Simply typed lambda calculus
3. Second order typed lambda calculus
4. Types dependent on types
5. Types dependent on terms
6. The Calculus of Constructions
7. The encoding of logical notions in λC
8. Definitions
9. Extension of λC with definitions
10. Rules and properties of λD
11. Flag-style natural deduction in λD
12. Mathematics in λD: a first attempt
13. Sets and subsets
14. Numbers and arithmetic in λD
15. An elaborated example
16. Further perspectives
Appendix A. Logic in λD
Appendix B. Arithmetical axioms, definitions and lemmas
Appendix C. Two complete example proofs in λD
Appendix D. Derivation rules for λD
Index of names
Index of technical notions
Index of defined constants
Index of subjects.