Lehrende: Prof. Dr. rer. nat. Kirstin Peters
Veranstaltungsart: Integrierte Veranstaltung
Orga-Einheit: FB20 Informatik
Anzeige im Stundenplan: TS
Fach:
Anrechenbar für:
Semesterwochenstunden: 4
Unterrichtssprache: Englisch
Min. | Max. Teilnehmerzahl: - | -
Lehrinhalte: Typsysteme bieten einen effizienten Weg, um die korrekte Funktionsweise von Programmen zu garantieren, bevor diese überhaupt gestartet werden. Es gibt sie in den verschiedensten Ausprägungen: als Standard-Konstrukt und Teil einer Programmiersprache oder speziell für bestimmte Anwendungen entworfen. Wir werden uns u.A. mit den folgenden Themen beschäftigen: - Einfach getypter lambda-Kalkül - Statische vs. dynamische Analyse von Typen - Operationale Semantik - Soundness von Typsystemen - Typ Inferenz - Curry-Howard-Korrespondenz - Polymorphism - Subtyping - Safety und Liveness Garantien durch Typsysteme - Abhängige Typen
Literatur: 'Types and Programming Languages' von Benjamin C. Pierce
Voraussetzungen: Informatik- und Mathematikkenntnisse entsprechend den ersten 4 Semestern des Bachelorstudiengangs Informatik, insbesondere grundlegende Logikkenntnisse und Fähigkeit, mit formalen Sprachen und Kalkülen umzugehen.
Offizielle Kursbeschreibung: Typsysteme sind integraler Bestandteil vieler Programmiersprachen und ein wichtiger Grundbaustein der Verifikation. Dieser Kurs liefert eine Einführung in Typsysteme. Es werden die grundsätzliche Konzepte, Stärken und Grenzen von Typsystemen diskutiert.
Online-Angebote: moodle
