The Semantics course covers topics in the theory of programming languages and program verification. The course material is fully mechanized in Coq and the accompanying mechanization contains templates for exercises in the lecture notes. The course is split into two parts.

The first part of the course is concerned with the basics of programming language theory: small-step semantics, big-step semantics, and type systems. It covers the semantics of programming languages with abstract data types, recursion, and mutable state. The main goal in this part is to prove semantic properties about these languages, in particular what is known as type safety. To address this goal, we use the technique of logical relations, which can be used to build expressive models of programming languages.

The second part of the course takes a different approach to programming language semantics, namely program logics. It covers Hoare logic, separation logic and, in particular, the separation logic Iris. It ties back into the first part of the course by defining a logical relation inside of Iris.