Review: A Modern Perspective on Type Theory: From its Origins until Today, by Fairouz Kamareddine, Twan Laan, and Rob Nederpelt
This brief description — largely borrowed from the book under review — shows an exciting evolution and convergence of ideas related to type theory. While many logicians seem to be aware of this story, many researchers are still only familiar with one side of it. For example, specialists in foundations of set theory are quite familiar with Russell’s type theory, and may be aware of intuitionistic mathematics, but they may not know much about the relation between intutionistic (constructive) logic and type theory. Specialists in theoretical computer science are usually quite familiar with recursive functions and λ-calculus, but
not with set-theoretical types and the use of PAT in proof checking. Specialists in programming languages may be familiar with types and type checking, but are usually not aware of the relation between these (practical) types and more theoretical work that they may have studied in Theory of Computations and AI classes. Specialists in AI are usually familiar with LISP—and maybe with proof checking software, but they are usually not aware of the deep relation between the two and of the relation between these subjects and foundations of set theory.
One reason why the relationship is not well known is that up to know, diﬀerent aspects of type theory were presented in diﬀerent forms, sometimes informally. The authors meticulously go over the past formalisms and approaches and describe them in a similar way, so that modern readers will be able to understand all the details of each formalism — and the relation between diﬀerent type theories and between their various applications.
The result is a very useful book