Main Page

News

No Tutorial on Wed, Dec 13

Written on 11.12.23 by Benjamin Peters

Dear all,

there will not be a tutorial (or a test) this Wednesday, Dec 13, due to the exam.

Next week's tutorial, on Dec 20, will cover both last week's lectures and the next lecture on Thursday, Dec 14.

Best,
Benjamin and Niklas

Tuesday office hours start 15:30

Written on 28.11.23 by Niklas Mück

Dear students,

due to a request, we will start office hours 30 minutes earlier on Tuesdays, i.e. at 15:30. Correspondingly, they will end at 16:30 if no students are present anymore. These changes are effective starting today and do not affect our Friday office hours at 14:00 - 15:00.

We hope… Read more

Dear students,

We hope that this change allows students having other classes starting at 16:00 to attend the Tuesday office hours.

Best,
Benjamin and Niklas

Lecture next Monday at 14:05

Written on 24.11.23 by Benjamin Peters

Dear all,

please be aware that the lecture on Monday, Nov 27, will start at 14:05 instead of the usual 14:15.

Best,
Your Semantics team

Tutorial is We 16-18 (in room 005 in E1 5) and Midterm is Mo 11. Dec during class

Written on 03.11.23 (last change on 06.11.23) by Niklas Mück

Dear all,

We have finally set the dates for the tutorial and the midterm.
- The midterm will take place on December 11th during class (i.e. 14:00–16:00).
- The weekly tutorial will take place every Wednesday from 16:15–18:00 in room 005 in E1 5 on the ground floor (the first room you will see… Read more

Dear all,

Just a reminder: We also have office hours every Tuesday from 16:00–17:00 and Friday from 14:00–15:00 in room 422 in E1 5. You can find us by either taking the elevator or the stairs to the fourth floor and then turning right.

If one of the dates does not work for you, please contact us as soon as possible.
Your Semantics Team

Tutorial times

Written on 25.10.23 (last change on 25.10.23) by Benjamin Peters

Dear all,

We have some important announcements regarding the tutorials and office hours.

Dear all,

We have some important announcements regarding the tutorials and office hours.

1. The time slots for tutorial we are currently considering are Wednesdays 10:15-12:00 or 12:15-14:00, potentially also 16:15-18:00. If you are not available at these times, send us an email and tell us what lecture/tutorial/… you have a conflict with. We will decide on a slot next week.
2. The first tutorial will be Tuesday, Oct 31 from 16:15-18:00 in E1.5 029. Next week the test will not be during the tutorial, but before the lecture on Thursday, Nov 2 from 14:14-14:30.
3. We noticed that many of you have a lecture conflicting with the office hours on Tuesdays at 14:00. Starting Nov 6, it will be at 16:00-17:00 instead.

You can find all of this information in the timetable.

Yours,
Niklas and Benjamin

Semantics

The course covers topics in the theory of programming languages and program verification. We assume that students are familiar with the proof assistant Coq. 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 Coq proof assistant to formally check our results during this course. We assume that you are familiar with the basic usage of Coq (for instance, as taught in the Introduction to Computational Logic Course at Saarland University).

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

Lectures

Lectures are on Mondays and Thursdays at 14:15-15:45 in the lecture hall 001 in E1.3.
The first lecture is on Monday, October 23, 2023.
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.

Every student can state their own preference on the personal status page after the first lecture.

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 Tuesdays at 4pm and Fridays at 2pm in E1.5 room 422.

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

If you have a question, just drop by! In the Friday office hour, we will discuss the Coq code accompanying the lecture.

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.