×

Lambda calculus with types. With contributions from Fabio Alessi, Henk Barendregt, Marc Bezem, Felice Cardone, Mario Coppo, Wil Dekkers, Mariangiola Dezani-Ciancaglini, Gilles Dowek, Silvia Ghilezan, Furio Honsell, Michael Moortgat, Paula Severi, Richard Statman, Paweł Urzyczyn. (English) Zbl 1347.03001

Perspectives in Logic. Cambridge: Cambridge University Press; Ithaca, NY: Association of Symbolic Logic (ASL) (ISBN 978-0-521-76614-2/hbk). xxii, 833 p. (2013).
In 1981 H. Barendregt published a book on lambda calculus [The lambda calculus. Its syntax and semantics. Rev. ed. York-Oxford: North-Holland (1984; Zbl 0551.03007); reprint, London: College Publications (2012; Zbl 1267.03034)] which is, still today, a standard reference in the field. The volume under review – edited together with Wil Dekkers and Richard Statman and written together with many further experts of the area – is not a revised version of the old book, but a complementary volume thoroughly presenting the lambda calculus augmented by types: “This book is about lambda terms typed using simple, recursive and intersection types. In some sense, it is a sequel to [Zbl 0551.03007]. That book is about untyped lambda calculus. Types give the untyped terms more structure. […] The extra structure makes the theory of typed terms quite different from the untyped ones.” (Preface, p. ix).
The book is divided into three parts on simple, recursive, and intersection types. (One may wonder whether the 833 pages could have been divided into three separate volumes, respectively.) It does not cover, however, some advanced topics as dependent types, higher-order (even second-order) types and inductive types. The authors refer (p. xxi) to [J.-Y. Girard et al., Proofs and types. Cambridge etc.: Univ. Press (1989; Zbl 0671.68002)] and [M. H. Sørensen and P. Urzyczyn, Lectures on the Curry-Howard isomorphism. Amsterdam: Elsevier (2006; Zbl 1183.03004)] for higher-order (better: second-order) types. We may add for dependent types the recent book [R. Nederpelt and H. Geuvers, Type theory and formal proof. An introduction. Cambridge: Cambridge University Press (2014; Zbl 1317.03001)].
In general, the book is of encyclopedic character, presenting all kind of variations of the different theories. It presents a firm mathematical foundation of the topic – in the compelling words of the authors: “We will study the formalism for its mathematical beauty.” (p. xxi). All Chapters finish with exercises which are valuable to involve the reader in the presented material.
A detailed presentation of applications would go beyond the scope of this book, but “a flavor of some” (p. xxi) is given in Chapter 6, notably functional programming, proof-checking, and formal semantics of natural languages.
This book will be a valuable reference for both beginners and experts in the field.
Let us here note one occurrence where the authors run into an error when transferring an old result of Kleene into the realm of second-order typed lambda calculus: the proof of Corollary 6.1.4 (p. 326) does not work in the present context. (The underlying issue is discussed in more length in [R. Matthes, Extensions of system F by iteration and primitive recursion on monotone inductive types. München: Utz Verlag; München: LMU, Univ. München, Fakultät Mathematik/ Informatik (1998; Zbl 0943.68086)]; the reviewer is grateful to Ralph Matthes to have pointed out to him this pitfall.)

MSC:

03-01 Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations
03B40 Combinatory logic and lambda calculus
03B15 Higher-order logic; type theory (MSC2010)
03D75 Abstract and axiomatic computability and recursion theory
03B70 Logic in computer science
PDF BibTeX XML Cite