Lecture notes with exercises for the introductory course on domain theory and denotational semantics at the Midlands Graduate School (MGS) 2023.
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.
The notes are available in full colour and black and white.
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.