Core Course (Theoretical Computer Science), 9 credit points
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 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.