Main Page

News

Warm-up Sheet Solutions & Exercise Sheet 1 Out

Written on 24.10.25 (last change on 25.10.25) by Laila Elbeheiry

Dear students,

We have released the solutions for the warm-up sheet and the new exercise sheet. Please make sure you pull the changes in the repo.

Note that the new exercise sheet and the old solutions will be released every Friday.

Enjoy!

Laila and Janine

Tutorial Time and Midterm Date

Written on 22.10.25 by Janine Lohse

Dear Students,

the midterm will be on December 10 during lecture time. The tentative tutorial time is on Thursdays, 16-18, starting next week, the test will be written in the beginning of the tutorial. Please note that you need to be here for the midterm and additionally score at least 50% in the… Read more

Dear Students,

Best,

Your Semantics Team

First Exercise Sheet

Written on 17.10.25 by Janine Lohse

Dear Students,

Welcome to Semantics! We just released the first exercise sheet, which is a warm-up sheet to familiarize you with the Rocq development for this course. In case you are not familiar with Rocq yet, please come talk to us in the Office Hour such that we can give you individual advise on how to catch up. The first office hour will be on Monday, October 20, 15:30-16:30 in building E1 5, room 005. In case you have trouble with the installation or other questions, also drop by at the office hour!

See you soon!

Your Semantics Team.

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

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.

Tutorials

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

Office Hours are offered weekly on Mondays, 15:30 - 16:30 in building E1 5, room 005.

You can come there to ask questions about the exercise sheets, topics discussed in the lecture, and the Rocq development accompanying the lecture.

If you have a question, just drop by!

Tests

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.

Registration

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.