Type Systems for Correctness and Security

Inhalt

Typsysteme in Programmiersprache helfen fehlerhaftes Verhalten von Beginn an zu vermeiden. Sie erlauben wertvolle Rückmeldungen für Entwickler, um Fehler und Systemabstürze zu vermeiden oder sogar Sicherheitslücken zu erkennen. In dieser Vorlesung werden wir Typsysteme entwickeln und untersuchen. Wir werden die Theorie behandeln, die Eigenschaften mit denen Typsysteme uns in der Softwareentwicklung unterstützen besprechen und die Implementierung aktueller Typsysteme untersuchen. Wir werden einen pragmatischen Ansatz durchführen und im Laufe der Vorlesung und im Rahmen von Übungen die Implementierung von Typcheckern er üben. Weiterhin untersuchen wir die Typsysteme von bekannten Programmiersprachen wie Java oder Scala genauer.

Literatur

Der Kurs basiert auf dem folgenden Buch:
Benjamin C. Pierce. 2002. Types and Programming Languages. The MIT Press.

Wir werden auch Themen aus diesem weiterführenden Buch behandeln:
Benjamin C. Pierce. 2004. Advanced Topics in Types and Programming Languages. The MIT Press. 

Weiteres Material wird in den Kursunterlagen angekündigt werden.

Vorlesung

• Die Vorlesungen werden jeden Donnerstag 15:30 - 18:00 Uhr auf Zoom stattfinden. Dazu findet sich jeweils in den entsprechenden Abschnitten in Moodle der passende Link. Sollten alle Teilnehmenden zustimmen können Aufzeichnungen erfolgen. 
• Die Sitzungen sind interaktiv. Sie können also jederzeit Fragen stellen. Machen Sie davon regen Gebrauch.
• Zusätzlich können die Aufnahmen des letzten Jahres auch in Moodle eingestellt werden.

Theoretische Übungsaufgaben

• Es wird begleitende Übungen zu den Vorlesungsinhalten in Form einer Videokonferenz geben. Diese Übung findet 7 Tage nach der Ausgabe des Übungsblatts statt um eine eigene Bearbeitung zu ermöglichen.
• Die Übungssitzungen finden in Zoom jeden Freitag 10:00 - 11:30 Uhr statt. Die Links finden Sie jeweils in Moodle. Auch hier können Aufnahmen gemacht werden, wenn Sie alle zustimmen.
• Ich bitte Sie dabei Ihre Kamera in Zoom aktiviert zu haben. Das hilft dabei die räumliche Distanz zumindest ein bisschen kleiner erscheinen zu lassen. 
• Diese Übungen werden nicht von uns korrigiert.
• 14 Tage nach der Übungsausgabe wird ein Lösungsvorschlag von uns zur Verfügung gestellt, den Sie für eine Selbstkorrektur nutzen können.
• Wir empfehlen jedoch mit Nachdruck diese Übungen zu machen, da Sie auf die Prüfung vorbereiten.
• Sie erhalten dadurch auch ein Gefühl für die Art der Fragestellung.
• Die Übungen finden Sie in Moodle jeweils zum passenden Thema.

Praktische Übungsaufgaben (Studienleistung)

• Es wird ein begleitendes Praktikum geben in dem die Vorlesungsinhalte praktisch vertieft werden. 
• Diese Programmierpraktika sind alleine und selbstständig durchzuführen.
• Die Abgabe findet über eine von uns bereitgestellte Abgabeplattform statt.
• Es ist notwendig mindestens 50% der erreichbaren Punkte zu erhalten, um für die Klausur zugelassen zu werden.

Kommunikation

• Jeden Montag 10:00 - 11:00 Uhr wird eine Sprechstunde in Zoom angeboten. Der Link für diese Sprechstunde findet sich bald im oberen Bereich in Moodle.
• Diese Sprechstunde ist explizit als Gruppensprechstunde konzipiert. Das heißt es sollte sich um Inhalte der Veranstaltung drehen.
• Ganz explizit bitte ich Sie dort auch Fragen zu den Übungs- und Praktikumsaufgaben zu stellen.
• Ich bitte Sie dabei Ihre Kamera in Zoom aktiviert zu haben. Das hilft dabei die räumliche Distanz zumindest ein bisschen kleiner erscheinen zu lassen. 
• Im Forum Fragen und Antworten in Moodle können Sie jederzeit eine Frage zur Veranstaltung stellen. Sie können auch jederzeit Fragen anderer Studierender dort beantworten. Ich werde die Diskussionen verfolgen und ggf. ergänzen und Fragen beantworten, die noch unbeantwortet geblieben sind. Ich bitte Sie von dieser Möglichkeit Gebrauch zu machen und sich hier gegenseitig bei der Erarbeitung des Stoffes zu helfen. Es ist wissenschaftlich erwiesen, dass nichts mehr dabei hilft eine Sache zu erlernen (oder zu festigen) als sie anderen Menschen zu erklären. 
• Wenn Sie ein persönliches Anliegen (z.B. in Bezug auf Anmeldungsformalitäten) haben, schreiben Sie mir bitte und bitten Sie um einen persönlichen Termin. 

Prüfung

 Wir sehen hier eine mündliche Prüfung vor. Im Fall von erhöhten Anmeldezahlen behalten wir uns vor schriftliche Prüfungen durchzuführen.