Teaching Denotational Semantics
Achim Jung · 2014
In 1969 Dana Scott suggested, [Sco93], that a Tarskian semantics could be given to programming languages by employing ordered structures of a certain kind, now known as domains. One of his key insights was that recursion can be modelled via the least fixpoint of endofunctions on domains. Shortly afterwards Gordon Plotkin, explored this proposal further; among the many results of his landmark paper [Plo77] he formulated and proved computational adequacy, which can be said to justify Scott’s least-fixpoint semantics. Much of the development of denotational semantics since then can be traced back to these two papers and few would contest their status as “classics” of our subject. 50 years later, one would expect to see Scott’s and Plotkin’s work reflected in the standard syllabus of computer science degrees around the world, on a par with other classic results of our subject, such as the relationship between automata and languages, the undecidability of the halting problem, and NP -completeness. This, however, is not the case, despite a clutch of excellent textbooks appearing in the late 1980s and early 1990s: [Sch86, Ten91, NN91, Gun92, Win93, Mit96]. Of the many possible reasons for this state of affairs, I believe the following are the most important: (a) the subject is notationally subtle and heavy at the same time, (b) students do not have enough mathematical background, (c) the “rewards” for the time and effort invested appear limited to the student. In this note I want to report on my own experiences of teaching denotational semantics, which has taken place in a variety of contexts and to some very different audiences, with my primary reference point being a five-lecture course delivered as part of the Midlands Graduate School in the Foundations of Computing Science (MGS), which since 2001 has taken place annually at one of the four partner universities: Birmingham, Leicester, Nottingham, and Sheffield.