Core course, 9 credit points
Final exam registrations: thread.
|First lecture:||Thursday, 17. October 2013|
|First tutorial:||Monday, 21. October 2013|
|Christmas break:||Thursday, 19. December 2013 until Friday, 03. January 2014|
|Last lecture:||Monday, 03. February 2014|
The course covers topics in the theory of programming languages. We assume that students are familiar with the proof assistant Coq.
- Abstract reduction systems
- Untyped lambda calculus, confluence
- Strong normalization of simply typed lambda calculus
- Calculus of constructions
- Inductive definitions
- Imperative languages and Hoare Logic
- Type inference
- Set theory
- PCF with recursive types
Lectures are on Mondays 10:15–12:00 and Thursdays 12:15–14:00, in Building E1 3, Lecture Hall 001. The first class is on Thursday, October 17.
There will be weekly tutorials, starting in the second week of term time. The tutorials will be on Mondays 16:15–18:00, in Building E1 3, Lecture Hall 003.
To receive credit points for this course, students must register for it with the University's HISPOS system. You must also register with us in order to take part in the tutorials and exams. Registration will be open between Sunday, 03. November 2013, 12:00 until Friday, 08. November 2013, 23:59. If you later decide to unregister, you must make sure to unregister with HISPOS and should also send an email to .