Computing Reviews

The formal semantics of programming languages
Winskel G., MIT Press,Cambridge, MA,1993.Type:Book
Date Reviewed: 08/01/94

The mathematics, techniques, and concepts of operational, denotational, and axiomatic semantics are presented. This introductory book is primarily addressed to undergraduate and graduate students, so it starts with basic material. But more advanced material on topics of recent research is also provided.

The book comprises 14 chapters. Basic notations of logic and set theory are given in the first chapter. Chapter 2 introduces the structural operational semantics for a simple imperative language of while programs, IMP. Detailed material on inductive proof principles and inductive definitions is provided in chapters 3 and 4. Chapter 5 continues with a denotational semantics for IMP and an equivalence proof of the introduced operational and denotational semantics. Chapters6 and 7 are devoted to the axiomatic Hoare-style semantics and completeness aspects of Hoare rules.

A detailed introduction to the theory of complete partial orders and &lgr;-notation is given in chapter 8. With the simple applicative language REC, supporting recursive definitions, chapter 9 discusses call-by-value and call-by-name evaluation of languages. Again, an operational and a denotational semantics and their equivalence for both cases are completely worked out. The treatment of recursive definitions is extended in chapter 10. The different semantic descriptions for languages with higher types, treating functions as first-order elements, follow in chapter 11, leading to the concept of full abstraction. The next two chapters are dedicated to recursive types. Recursive domain equations are solved by information systems.

The last chapter treats parallelism and nondeterminism, including guarded commands, calculus of communicating systems (CCS), and local model checking. An appendix contains a brief introduction to the theory of computation, based on a notation of A. Meyer, which is used for chapters1 through 7.

This carefully written book achieves its purpose of being an introductory book on semantics, leading the reader from basic material to recent research topics. The text is accompanied by exercises of varying difficulty. At the end of each chapter, the author cites original works on which the presentation is based and gives further readings. I recommend this book not only as a basis for introductory courses but also for independent study by people interested in semantics.

Reviewer:  Gudula RĂ¼nger Review #: CR117419

Reproduction in whole or in part without permission is prohibited.   Copyright 2024 ComputingReviews.com™
Terms of Use
| Privacy Policy