Formal Semantics ─ An Introduction

The Formal Semantics of Programming Languages provides the basic mathematicaltechniques necessary for those who are beginning a study of the semantics and logics of programminglanguages. These techniques will allow students to invent, formalize, and justify rules with whichto reason about a variety of programming languages. Although the treatment is elementary, several ofthe topics covered are drawn from recent research, including the vital area of concurency. The bookcontains many exercises ranging from simple to miniprojects.Starting with basic set theory,structural operational semantics is introduced as a way to define the meaning of programminglanguages along with associated proof techniques. Denotational and axiomatic semantics areillustrated on a simple language of while-programs, and fall proofs are given of the equivalence ofthe operational and denotational semantics and soundness and relative completeness of the axiomaticsemantics. A proof of Godel's incompleteness theorem, which emphasizes the impossibility ofachieving a fully complete axiomatic semantics, is included. It is supported by an appendixproviding an introduction to the theory of computability based on while-programs.Following apresentation of domain theory, the semantics and methods of proof for several functional languagesare treated. The simplest language is that of recursion equations with both call-by-value andcall-by-name evaluation. This work is extended to lan guages with higher and recursive types,including a treatment of the eager and lazy lambda-calculi. Throughout, the relationship betweendenotational and operational semantics is stressed, and the proofs of the correspondence between theoperation and denotational semantics are provided. The treatment of recursive types - one of themore advanced parts of the book - relies on the use of information systems to represent domains. Thebook concludes with a chapter on parallel programming languages, accompanied by a discussion ofmethods for specifying and verifying nondeterministic and parallel programs.

Glynn Winskel is Professor of Computer Science at the University of Aarhus, Denmark.