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 Monday, December 7. The second part ends with a final exam on Friday, February 19.
The first part covers lambda calculus and type theory.
The second part covers the semantics of practical programming languages with abstract types, recursion, and mutable state.
Lectures are on Mondays 14:15–15:45 and Fridays 12:15–13:45, in Building E1 3, Lecture Hall 002. First lecture is on Friday, October 23, 2015. See the timetable for more details.
There will be weekly tutorials.
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.