Domain theory and denotational semantics

Lecture notes with exercises for the introductory course on domain theory and denotational semantics at the Midlands Graduate School (MGS) 2023.

Abstract

Denotational semantics aims to understand computer programs by assigning mathematical meaning to the syntax of a programming language. In this course we will study a simple functional programming language called PCF. Notably, this language has general recursion through a fixed point operator. This means a simple denotational semantics based on sets is not suitable. Instead, we interpret the types of PCF as certain partially ordered sets leading to domain theory and Scott's model of PCF in particular. The central theorems of soundness and computational adequacy, formulated and proved by Plotkin, then tell us that a PCF program computes to a value if and only if their interpretations in the model are equal.

Links to the notes

The notes are available in full colour and black and white.

Fixing inaccuracies

If you find an inaccuracy of any kind in the notes, then please help me fix it:

• If you know how to fix it and are comfortable using GitHub, please consider making a pull request with your fix.
• If you don't know how to fix it and are comfortable using GitHub, please consider creating an issue addressing the inaccuracy.
• If you don't wish to use GitHub, please inform me of the inaccuracy by sending me an email at tom.dejong[symbol]nottingham.ac.uk.

Post-lecture feedback

Your feedback is anonymous and will be used to improve future lectures.

1. Feedback form for Lecture 1
2. Feedback form for Lecture 2
3. Feedback form for Lecture 3
4. Feedback form for Lecture 4

---

My homepage