Domains and lambda-calculi. (English) Zbl 0962.03001

Amadio, Roberto M.; Curien, Pierre-Louis

Cambridge Tracts in Theoretical Computer Science. 46. Cambridge: Cambridge University Press. xvi, 484 p. (1998).

This book is about domain theory with applications to the syntax of lambda calculus. This is an excellent, thorough monograph. As a rich and comprehensive source of information, it is very useful as a reference to classical results in domain theory and lambda calculus. The presentation is rather dense and many standard results are shown in exercises. The reader should better have a firm background in mathematical structures as well as a basic knowledge in recursion and category theory despite the two appendices on these latter topics. Though it could be used as a textbook for an advanced course for graduate students in computer science, it seems more suitable for students in mathematics with interest in theoretical computer science. The book is organized in 16 chapters and two appendices on Recursion Theory and Category Theory. Semantics and syntax are alternated along the chapters. The general way of presentation consists in first showing the semantics and then defining the corresponding syntax together with an intepretation. The subject of domain theory is presented from an introductory basis and includes the construction of Scott’s model D1 (chapter 3), bifinite domains, L-domains (chapter 5), solution of domain equations, universal domains (chapter 7), powerdomains (chapter 9), stability on meet cpo’s, dI-domains, continuous L-lattices (chapter 12), models for linear logic (chapter 13) and sequentiality (chapter 14). The corresponding list of lambda calculi and logics that are interleaved with the previous semantic concepts are completely defined in the book and includes: pure lambda calculus (chapter 2), intersection types (chapter 3), simply typed lambda calculus (chapter 4), the language PCF (chapter 6), a call-by-value and parallel lambda calculus, continuations (chapter 8), Milner’s CCS (chapter 9), the second order typed lambda calculus and the system LF of dependent types (chapter 11), linear logic (chapter 13), an extension of PCF (chapter 14) and ss-calculus (chapter 16).

Reviewer: Paula G.Severi (Montevideo)

MSC:

03-02	Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
68-02	Research exposition (monographs, survey articles) pertaining to computer science
03B40	Combinatory logic and lambda calculus
68Q55	Semantics in the theory of computing
03B70	Logic in computer science

Keywords:

domain theory; syntax of lambda calculus; semantics; syntax