Semantics

The course covers topics in the theory of programming languages and program verification. We assume that students are familiar with the proof assistant Rocq. The course is split into two parts.

 

In the first part, we will start with the basics of programming language theory: small-step semantics, big-step semantics, and type systems. We will discuss the semantics of practical programming languages with abstract types, recursion, and mutable state. The goal will be to prove semantic properties about these languages. To this end, we will discuss the technique of logical relations which can be used to build expressive models of programming languages. The first part ends with a midterm exam.

 

In the second part, we will follow a different approach to programming language semantics: the axiomatic approach put forth by program logics. We will discuss the program logic Iris and how it can be used for program verification. Towards the end of the second part, we will consolidate the axiomatic approach with what we have learned in the first part. That is, we will discuss how to build expressive logical relations in Iris. The second part ends with a final exam whose date will be announced during the course.

 

We will be using the Rocq proof assistant to formally check our results during this course. We assume that you are familiar with the basic usage of Rocq (for instance, as taught in the Introduction to Computational Logic Course at Saarland University).

 

The following video is a presentation of a previous iteration of the course.

Lectures are on Wednesdays and Fridays at 10:15-11:45 in Building E1.3, Lecture Hall 001.
The first lecture is on Wednesday, October 15, 2025.
See the timetable for more details.

 

There will be a weekly tutorial. The precise time slot will be picked according to the students' preference.

 

In the tutorials, you can test your knowledge in an exam-like situation (tests, see below), discuss the sample solutions to the assignments with your tutor and your fellow students, and get hints and suggestions concerning the lecture. A tutorial usually takes about 90 minutes.

 

Office Hours are offered weekly, date and time are TBD.

Tests allow you to practice your skills in an exam-like situation.

 

Tests will be offered at the beginning of each tutorial. They are written and closed-book, and examine the contents of the current assignment sheet. Tests will take 15 minutes. To prepare for the tests, you should work through the assignments, and use the office hours and the discussion board to ask about anything that is unclear to you.

 

Tests will be graded. In each test you can gather up to 15 points. Missing a test gets you 0 points for that test.

 

You need to gather a certain minimum of points in the tests to be admitted to the exams. See the exams page for details.

 

Your test scores can be found on your personal status page.

 

To take part in the course, please register with us (top of the page).
To receive credit points for this course, students must register with the University's HISPOS system.