Semantics Derek Dreyer

News

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.
The Wednesday office hour is hybrid and the Friday office hour is virtual. 
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.


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