Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Programming language theory and its implementation
Gordon M., Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1988. Type: Book (9789780137304172)
Date Reviewed: Jul 1 1989

This text should be considered for an introductory course in programming language theory and implementation for advanced undergraduates or beginning graduate students. The author presents a concise overview of methods, issues, and developments in both imperative and functional language verification. His discussion is evenhanded and does not get bogged down in details or theory. The book contains numerous examples and exercises that reinforce material immediately after it has been presented and ends with a good bibliography. Gordon provides an informative historical sketch of the relevance of the lambda calculus to contemporary functional program verification theory, as well as some historical commentary on LISP.

Part 1 presents the axioms and rules of Floyd-Hoare logic, illustrating them on a small Pascal-like programming language, and offers an approach to mechanizing program verification. The semantics of WHILE commands is badly botched near the beginning of the book. Fortunately, the book appears relatively free of errors otherwise.

Part 2, “The Lambda Calculus and Combinators,” begins with an introduction to the syntax and semantics of the lambda calculus, then discusses how the lambda calculus can represent various data objects and recursive functions. The author illustrates functional programming with a small functional programming language and presents an algorithm to compile from this language into lambda expressions. A chapter on combinators, which includes an introduction to reduction machines and algorithms (due to Curry and Turner) for compiling lambda expressions into combinators, concludes this part. In a separate chapter, the author presents the Church-Rosser and normalization theorems, and the theorem on the undecidability of the halting problem, and explains their significance for functional language implementation theory.

Part 3 contains a brief introduction to LISP that includes a discussion of the advantages and disadvantages of dynamic binding. The author then provides code in Franz LISP for a simple theorem prover, a program verifier, and a lambda calculus toolkit (parser, reducer, and translator to combinators). Each section of code is explained. I keyed in and ran the theorem prover (using LISZT VAX version 8.36): the example on page 192 did not, however, evaluate to T as it should have. Instead, the theorem prover wrote out the original implication, substituting X for each occurrence of 1, which gave

:.PD8 :.OC :.HB (((X=(((N − X) * N) DIV 2) and ((X <= N) and (N <=M )))

implies ((X + N)=(((N + X) − X) * (N + X)) DIV 2))).:.OE :.HT

Reviewer:  Nicholas Ourusoff Review #: CR112971
Bookmark and Share
Would you recommend this review?
Other reviews under "General": Date
Programming languages
Dershem H. (ed), Jipping M., Wadsworth Publ. Co., Belmont, CA, 1990. Type: Book (9780534129002)
Jan 1 1992
Thinking recursively with Java
Roberts E., John Wiley & Sons, New York, NY, 2005.  192, Type: Book (9780471701460)
Jun 6 2006
Online programming languages and assemblers: a reference
Birnes W. (ed), McGraw-Hill, Inc., New York, NY, 1989. Type: Book (9780070053953)
Mar 1 1990

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