Type Systems for Correctness and Security

Course Content

Type systems help to avoid errors in programs from the very beginning. They allow for valuable feedback for developers to avoid bugs and system crashes or even to detect security vulnerabilities. In this lecture we will develop and study type systems. We will cover the theory, discuss the properties with which type systems assist us in software development, and examine the implementation of current type systems. We will take a pragmatic approach and practice implementing type checkers during the course of the lecture and exercises. Furthermore, we will examine the type systems of well-known programming languages such as Java or Scala in more detail.

Literature

The course is based on the following book:
Benjamin C. Pierce. 2002. Types and Programming Languages. The MIT Press.

Selected topics are based on this :
Benjamin C. Pierce. 2004. Advanced Topics in Types and Programming Languages. The MIT Press. 

Further reading material will be announced throughout the course.

Lecture

• The session is interactive. So you can ask questions at any time. Feel free to do so.
• Additionally, the recordings from previous years courses are available.

Theoretical Exercises

• There will be accompanying exercises to the lecture content 7 days after the exercise sheet is available, so you have time to work on it yourself.
• These exercise sheets will not be corrected by us.
• 14 days after the exercise is issued, we will provide a suggested solution that you can use for self-correction.
• However, we strongly recommend doing these exercises as they prepare you for the exam.
• It will also give you a feel for the nature of the questions.
• You can find the exercises in Moodle for the appropriate topic in each case.

Practical Exercises (Course Credit!)

• There will be an accompanying practical course in which the lecture contents will be deepened practically. 
• These programming practicals are to be carried out alone and independently.
• The submission will take place via a submission platform provided by us.
• It is necessary to get at least 50% of the achievable points to be admitted to the exam.

Communication

• In the forum Questions and Answers in Moodle you can ask a question about the course at any time. You can also answer questions from other students there at any time. I will follow the discussions and add to them if necessary and answer questions that are still unanswered. I ask you to make use of this opportunity and help each other here in working out the material. It is scientifically proven that nothing helps to learn (or consolidate) a thing more than explaining it to other people. 
• If you have a personal concern (e.g. regarding registration formalities), please write to me and ask for a personal appointment. 

Exams

Exams will be oral examinations or written exams (depending on number of participants)