Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
The formal semantics of programming languages
Winskel G., MIT Press, Cambridge, MA, 1993. Type: Book (9780262231695)
Date Reviewed: Aug 1 1994

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
Bookmark and Share
 
Semantics Of Programming Languages (F.3.2 )
 
 
Assertions (F.3.1 ... )
 
 
Pre- And Post-Conditions (F.3.1 ... )
 
 
Mathematical Logic (F.4.1 )
 
 
Modes Of Computation (F.1.2 )
 
Would you recommend this review?
yes
no
Other reviews under "Semantics Of Programming Languages": Date
Contractions in comparing concurrency semantics
Kok J. (ed), Rutten J. Theoretical Computer Science 76(2-3): 179-222, 2001. Type: Article
Aug 1 1991
Abstract language design
Bradley L. Theoretical Computer Science 77(1-2): 5-26, 1990. Type: Article
Nov 1 1991
Determinism → (event structure isomorphism = step sequence equivalence)
Vaandrager F. Theoretical Computer Science 79(2): 275-294, 1991. Type: Article
Dec 1 1991
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy