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 Sitzungen sind interaktiv. Sie können also jederzeit Fragen stellen. Machen Sie davon regen Gebrauch.
• Zusätzlich können die Aufnahmen der letzten Jahre auch in Moodle eingestellt werden.

Theoretische Übungsaufgaben

• Es wird begleitende Übungen zu den Vorlesungsinhalten geben. Diese Übung findet 7 Tage nach der Ausgabe des Übungsblatts statt um eine eigene Bearbeitung zu ermöglichen.
• 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

• 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.