Browse Books

Reviewer: Michael J. Oudshoorn

Robert Harper, from Carnegie Mellon University, has produced the second edition of the book Practical foundations for programming languages . The book is comprehensive in its coverage of the topic, which is divided into 19 parts and 49 chapters. The first part provides the basis for the book and covers chapters on abstract syntax, inductive definitions, and hypothetical and general judgment. From here, the reader is led through a comprehensive tour of programming language features, ranging from type systems and evaluation to modularity and process equivalence. Harper covers a wide range of topics in surprising depth within a book that is relatively short. This means that the book is dense and relies heavily on a rigorous mathematical basis established in the opening chapters. It is, consequently, precise in its definition and description of topics. There is not a great deal of textual support to aid the reader with the mathematical descriptions and so this book is best suited for graduate students and professionals who have a suitable mathematical and logic background. Readers uncomfortable with the mathematical notation and basis will struggle with the book. However, readers with the appropriate background will benefit from the precision offered by the book, and its encyclopedic breadth of coverage of programming language features. This book is not necessarily one that should be read cover to cover. It serves as an excellent reference and, provided the reader is familiar with the formal notation used, readers can skip to the chapters of interest/relevance to them. As indicated above, the book opens with an introduction to the mathematical notation used throughout. The coverage of programming languages commences with a discussion on static and dynamic aspects of type systems. This focus on static and dynamic aspects of language features, repeated in many of the chapters that follow, helps to provide a framework, making navigation throughout the book much easier. After type systems, Harper moves on to functions followed by finite data types. He then turns his attention to constructive logic and classical logic as applied to types and proposition, before proceeding to generic programming and inductive and coinductive types. After covering polymorphism and abstract types, Harper examines recursive functions and types before looking at dynamic types, including ?-calculus, dynamic typing, and hybrid typing. The next three parts cover subtyping, dynamic dispatch, and control flow, including exceptions. Symbolic data and mutable state, including lazy evaluation, are discussed in the next two parts before parallelism, concurrency, and distribution are addressed. Modularity and equivalence complete the book. The chapters are short, to the point, and grouped together appropriately into parts. The structure makes it relatively easy to find specific topics of interest, but be prepared for brevity. Online Computing Reviews Service