Main Page

News

Endterm results and inspection

Written on 16.02.22 by Simon Spies

Dear students,

we have finished grading the final exam. Well done! You can find your points and you grade on your personal status page.

The exam inspection will take place on Friday, February 25, at 1pm in room 005 of the MPI-SWS building. If this does not work for you and you would like to inspect your exam on another day, please let us know (via mail).

We really enjoyed the course and hope you did as well!

See you soon,
your Semantics Team

Lecture Room Change

Written on 14.12.21 by Simon Spies

Dear students,

starting tomorrow, we will use a different room for the lectures: Room 029 in the MPI-SWS (E1.5). The room is better equipped for hybrid lectures and, hopefully, attending virtually can become as engaging there as attending physically.

If you want to attend virtually, nothing… Read more

Dear students,

If you want to attend virtually, nothing changes for you tomorrow.

If you want to attend in-person, please come to the front gate of MPI-SWS between 10:00 and 10:15. There, one of us will need to verify your 2G status and, subsequently, you may enter the building. (Unfortunately, we have to keep a record of your attendance and the fact that we have verified your 2G status.)

Your Semantics Team

Midterm results and inspection

Written on 08.12.21 by Simon Spies

Dear students,

the results of the Midterm are now available on your personal status page in the CMS.

You can inspect your exam in Friday's office hour.
The exam inspection will only be possible in-person (in 005 at MPI-SWS).
If you cannot attend in person or have a conflict in that time slot,… Read more

Dear students,

the results of the Midterm are now available on your personal status page in the CMS.

Your Semantics Team

Room changes: hybrid tutorial today and office hour tomorrow

Written on 18.11.21 by Lennard Gäher

Dear students,

due to some logistic problems on short notice, today's tutorial is moved to room 029 in E1.5 (the MPI-SWS building).
As the building's entrance is not visible from 029, please be there on time by 16:10, so we can let you into the building.
If you come late, please briefly join the… Read more

Dear students,

Also note that, as announced previously, tomorrow's office hour is moved to room 422, where the same applies regarding getting into the building (let us know via Zoom when you are in front of the building, so we can come open the door).

Sorry for the inconvenience.

Your Semantics Team

Hybrid tutorial tomorrow

Written on 10.11.21 by Lennard Gäher

Dear students,

as already announced in the lecture today, due to popular demand tomorrow's tutorial will be the first one we offer in a hybrid format. This means that you can attend both in-person and, as previously, online via Zoom (if you plan to attend via Zoom, nothing changes for you).

The… Read more

Dear students,

The physical tutorial will take place in room 005 in the MPI-SWS building (E1.5), which is already known from the office hours. We have room for 11 participants. As access to the MPI-SWS building is currently still restricted, we have to open the building's door for you. Thus, please be there in time (by 16.10). We can see the door from the room, so if you come late, we should be able to see you and open the door for you (if we fail to do so, please briefly join the Zoom room and let us know). Moreover, due to the in-place contact tracing requirements, you have to enter the Visitor list at the entrance.

The test will, as usual, start at 16.15. For in-person participants, we provide print-outs.

We look forward to seeing you tomorrow!

Your Semantics Team

Tutorial Slot and Weekly Tests

Written on 27.10.21 by Lennard Gäher

Dear students,

thank you for filling out the poll for the tutorial slot. The slot that turned out to work best for most students is *Thursday, 4:15pm* (sharp). You can attend the tutorials online via Zoom (using the same link as the lectures). In the tutorials, we will discuss the lecture's… Read more

Dear students,

Please remember that there will be a 15min test at the beginning of the tutorials and that a sufficient number of points in the tests is required to be admitted to the exams. Please show up in time. The test will be unlocked at 16:15 on the materials page. You then have 15 minutes time to work on it, and an additional 5 minutes to upload it to your personal status page.

We expect you to be online in the Zoom room for the duration of the test.

Thanks,

Your Semantics Team

Poll on tutorial slot

Written on 20.10.21 by Lennard Gäher

Dear students,

as already announced in the first lecture today, you can find a poll for your tutorial slot on the personal status page. Please fill out the poll until Monday, 23.59, so we can determine a tutorial slot.

We have noticed that there are some conflicts in the options some of you have… Read more

Dear students,

We have noticed that there are some conflicts in the options some of you have chosen already. Since there will only be one tutorial, please choose the "Not okay" option only if you have a hard constraint and really cannot make this slot.

Thanks,

Your Semantics Team

Information for the First Lecture

Written on 18.10.21 by Simon Spies

Dear students,

We are excited that the first Semantics lecture is just around the corner. It will be on Wednesday, October 20, at 10 c.t. in HS002, E1.3. We would really like to meet you there! However, if you prefer to attend the lecture remotely, you can join via Zoom. To do so, please go to… Read more

Dear students,

We look forward to seeing you on Wednesday!
Derek, Simon, and Lennard

(As always, please obey the university's hygiene regulations: in particular 3G, and you have to register using the Staysio app when entering the lecture hall.)

Show all

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 on December 08.

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.

Lectures

Lectures are on Wednesdays 10:15-11:45 and Fridays 10:15-11:45 in the lecture hall 002 in E1.3.

Virtual participation in the lectures is possible via Zoom.
The first lecture is on Wednesday, October 20, 2021.
See the timetable for more details.

Tutorials

There will be a weekly tutorial on Thursdays.

The tutorial will happen online and 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 Mondays and Fridays, 1pm-3pm.

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.

The office hours on Mondays are virtual.

The office hours on Fridays are hybrid: you can attend physically in room 005 in the MPI-SWS building (E1.5) (except for November 19, where it's room 422).

E1.5 is not openly accessible right now, and you can enter it through one of the following ways:

You can wait at 13:15 in front of E1.5 and we will let everyone in.
We will usually see people waiting in front of the building from 005 and open the door for you. Otherwise, please briefly join the Zoom room to make us aware that you are waiting.
You can ask the porter in the MPI-INF building.

When entering E1.5, you need to register in the Visitor list.

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.