Theoretical computer scientists seek to understand programming by providing semantics for programming languages; they seek to identify the mathematical objects that programs denote. Because programs denote very complex mathematical objects, theoreticians study simplified programming languages, particularly programming languages with a mathematical flavor. In this book, Amadio and Curien consider several variations of the lambda calculus and develop domain theory to provide semantic models for these languages.

The authors begin with directed complete partial orders and define what it means for a function that maps one directed complete partial order into another to be continuous. Building on these notions, they establish links to topology and recursion theory, showing that computability is equivalent to continuity. They introduce both typed and untyped versions of the lambda calculus and include several features found in practical programming languages, such as continuations, fixpoints and arithmetic operators, call-by-value, exceptions and other control operators, dependent and second-order types, concurrency, and synchronization operators. For most of these features, the authors present mathematical models that capture the essence of the features, prove theorems about their properties, and frequently establish connections between these models and more syntactic approaches to semantics, which are referred to as operational semantics. In the last chapter, however, they discuss languages for concurrency, enriching lambda calculus with parallel composition and synchronization operators, but they do not present a denotational theory for them. In denotational semantics, this is an area that is just beginning to be explored.

This book is intended to be a textbook and, as such, is suitable for an advanced course in the denotational semantics of programming languages. Most of the theorems are proven in full; only a few are outlined by giving hints. Many exercises are interspersed throughout each chapter. Although there is an appendix summarizing recursive function theory and another appendix summarizing category theory, the reader should be familiar with these topics before attempting this book. Fortunately, the sources of the concepts and theorems covered in this book are meticulously cited, so the reader can consult them if necessary. Overall, the book is well written and will be clear to readers with sufficient mathematical maturity.