Saarland University Computer Science

Semantics Derek Dreyer and Gert Smolka

Core Lecture, 9 credit points, Winter Semester 2017

Registration for this course is open until Friday, 20.10.2017 23:59.

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:15.
The second part ends with a final exam on TBD.

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:00-15:00, E1 3, 525.

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.