A Practical Introduction to Denotational Semantics

Cambridge Computer Science Texts

by Lloyd Allison

This textbook is an introduction to denotational semantics and its applications to programming languages. Dr Allison emphasizes a practical approach and the student is encouraged to write and test denotational definitions. The first section is devoted to the mathematical foundations of the subject and sufficient detail is given to illustrate the fundamental problems. The remainder of the book covers the use of denotational semantics to describe sequential programming languages such as Algol, Pascal and C. Throughout, numerous exercises, usually in Pascal, will help the student practise writing definitions and carry out simple applications. The book culminates in discussing an executable semantics of the logic-programming language Prolog. Being an introduction, advanced undergraduates in computer science and graduates new to the subject will find this a readily accessible account of one of the central topics of computer science.

Genres: Mathematics

148 pages, Paperback

First published January 1, 1986

Reviews

[Tim Robinson · Rating 5 out of 5]

I cut my teeth on Scott-Strachey Denotational Semantics, which used little more that Set Theory as its object language. But this book is based on Polymorphic Typed Lambda Calculus, which is actually a richer language than the one I am trying to define! Also, the fact that the meaning of a program is a mathematical object is lost. Semantics as given here merely translates from one programming language to another: it is a compiler. The beauty of the Set Theory formalism is that it provides an escape from computer science to a world where thing are proved rather than executed.

Nevertheless, it is a useful refresher, and it does lay out the notation I require.

This book was written using Pascal and Algol-68 as teaching languages. Younger readers might find that more difficult than I did.

[Carter · Rating 3 out of 5]

Not as comprehensive or as rigorous as Stoy. Makes mention of Milner's CCS in the final chapter.