NewsCurrently, no news are available
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 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.
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.