Saarland University Computer Science

Core Course (Theoretical Computer Science), 9 credit points

Winter Semester 2009/2010

Prof. Gert Smolka, Dr. Jan Schwinghammer, Christian Doczkal
Department of Computer Science, Saarland University


This course introduces basic concepts and techniques in the foundational study of programming languages and interactive verification systems. The central theme is the view of individual programs and whole languages as mathematical objects about which precise claims may be made and proved. Particular topics include operational techniques for formal definition of language features, type systems and typed lambda calculi, polymorphism and subtyping, type reconstruction, and the correspondence between proofs and programs (Curry-Howard correspondence). We will introduce Coq, an interactive system combining specification, programming and proving. The concepts and techniques of this course have important applications in language design, compilers, security, software engineering, and system verification.

The 2003, 2005, and 2007 editions of this course.

Lectures and tutorials

Lectures are Monday and Wednesday, 10.15–12.00, HS 001 (Building E1 3)
First lecture: Wednesday, October 14, 2009

There will be weekly tutorials, Tuesday 16.15-17.45 in room 016 (Building E1 3).


To receive credit points for this course, students must register for it with the HISPOS software of the examination office. You must also register with us in order to take part in the tutorials and exams.
If you decide later to unregister, you must make sure you unregister with HISPOS and should also send an email to Jan Schwinghammer.

Last Change: Thu 01 Jan 1970 00:00:00 UTC |