Semantics Derek Dreyer and Gert Smolka

Core Lecture, 9 credit points, Winter Semester 2017

The course covers topics in the theory of programming languages. We assume that students are familiar with the proof assistant Coq.  The course will consist of two parts, the first given by Gert Smolka and the second given by Derek Dreyer.
The first part ends with a midterm exam on Thursday, December 7, 12:05-13:55.
The second part ends with a final exam on Friday, February 16, 14:00-16:00.

The first part covers ​basic semantic techniques (e.g., small-step and big-step semantics), IMP (an idealised imperative language), abstract reduction systems, and untyped lambda calculus (call-by-value and pure). The emphasis will be on proving semantic properties.

The second part covers the semantics of practical programming languages with abstract types, recursion, and mutable state.

Lectures are on Tuesdays 12:15 - 13:45 and Thursdays 12:15–13:45, in Building E1 3, Lecture Hall 002. First lecture is on Tuesday, October 17, 2017.  See the timetable for more details.

There will be weekly tutorials, Wednesday 16:15-18:00, in E2 4, SR 8 (318).
Office Hours are offered Tuesday, 14:15-15:45, E1 3, 525.
From December 19, the office hours will be in E1 5, 512 (5th floor of the MPI-SWS building).

Registration.  To take part in the course, please register with us (see menu on the left).  To receive credit points for this course, students must register with the University's HISPOS system.