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.