Core course, 9 credit points
Prof. Gert Smolka,
Dr. Chad E. Brown
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.
Lectures are on Mondays and Wednesdays, 10.15–12.00, in HS 003 (Building E1 3). The first lecture is on Wednesday, October 19, 2011.
There will be weekly tutorials, starting in the second week of term time.
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.
If you decide later to unregister, you must make sure to
unregister with HISPOS and should also send an email to Chad Brown.