Semantics Derek Dreyer

News

18.11.2021

Room changes: hybrid tutorial today and office hour tomorrow

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... Read more

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 Zoom room to let us know that we need to open the door.

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

10.11.2021

Hybrid tutorial tomorrow

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... Read more

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 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

27.10.2021

Tutorial Slot and Weekly Tests

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,... Read more

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 contents, talk about last week's exercises, and work on new exercises.

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

20.10.2021

Poll on tutorial slot

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... Read more

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 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

18.10.2021

Information for the First Lecture

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... Read more

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 "Information->Materials" and use the Zoom link that you find there.

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.)

 

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 Wednesdays 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 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.


Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators