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.
Lectures
Lectures are on Wednesdays, 12:15-13:45, and Friday, 12:15 - 13:45, in Building E1 3, lecture hall HS 002. The first lecture is on Wednesday, October 16. There will be no class on Friday, November 1, and between Wednesday, December 25, and Friday, January 3. See the timetable for all scheduled lectures.
Tutorials
There will be a weekly tutorial, Tuesday 12:15-13:50 in seminar room 4 (U.16) of building E2 5. The first tutorial is on October 22.
In the tutorials, you can
- test your knowledge in an exam-like situation (tests, see below),
- discuss the sample solutions to the assignments with your tutor and your fellow students, and
- get hints and suggestions concerning the lecture.
A tutorial usually takes about 90 minutes.
Office Hours
During the office hours, you can get direct support. You may, for example, want to
- resolve individual problems you might have with the lecture,
- discuss alternative solutions to the assignments,
- ask advanced questions about the contents of the lecture.
Office hours will normally take place on Mondays, 13:00-15:00, in room 528 of building E1 3. There might be additional office hours which you can find on the timetable.
Discussion Board
We offer a discussion board for the course.
All official announcements concerning the course will be made through the board exclusively. Therefore we require all students attending the course to subscribe to the board and frequently read the relevant sections.
Tests
Tests allow you to practice your skills in an exam-like situation.
Tests will be offered at the beginning of each tutorial. They are written and closed-book, and examine the contents of the current assignment sheet. Tests will take 15 minutes. To prepare for the tests, you should work through the assignments, and use the office hours and the discussion board to ask about anything that is unclear to you.
Tests will be graded. In each test you can gather up to 15 points. Missing a test gets you 0 points for that test.
You need to gather a certain minimum of points in the tests to be admitted to the exams. See the exams page for details.
Your test scores can be found on your personal status page.
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.