Typsysteme
Aktuelles
Inhalt
Typen dienen in Programmiersprachen dazu, Fehler bei der Übersetzung eines Programms abzufangen, die Übersetzung von überladenen Operatoren zu implementieren, die Lesbarkeit des Programmcodes zu erhöhen und bei der Suche einer gewünschten Funktion in einer Bibliothek zu helfen. Fortgeschrittene Typsysteme werden für die statische Analyse von Programmen verwendet, z.B. in Übersetzern, und um gewisse Programmeigenschaften zu spezifizieren und automatisch zu überprüfen.
In der Vorlesung wird in die Theorie der Typsysteme eingeführt. Es werden allgemeine Methoden für Typüberprüfung und Typinferenz behandelt und verschiedene Typsysteme vorgestellt, unter anderem: Typsysteme für funktionale und objektorientierte Sprachen; Typsysteme für Polymorphismus; abhängige Typen, mit denen sich vollständige Spezifikationen notieren lassen.
Organisation
- Umfang: 3+2 Semesterwochenstunden
- Für: Vertiefende Themen Bachelorstudiengänge Informatik; Master Informatik; Diplomstudiengänge Informatik
- Voraussetzung: Grundstudiumsvorlesungen der Informatik
- Vorlesung: Dr. Andreas Abel, Dr. Ulrich Schöpp
- Übungen: Dr. Andreas Abel
Zeit und Ort
| Veranstaltung | Zeit | Ort | Beginn |
|---|---|---|---|
| Vorlesung | Di, 14 - 16 Uhr | Hörsaal U139 (Oettingenstr. 67) | 03.05.2011 |
| Vorlesung | Do, 16 - 17 Uhr | Hörsaal 057 (Oettingenstr. 67) | 05.05.2011 |
| Übung | Do, 17 - 19 Uhr | Hörsaal 057 (Oettingenstr. 67) | 05.05.2011 |
Vorläufige Planung
| Datum | Typ | Thema | Material |
|---|---|---|---|
| Di 03.05. | V2 | [AA] Einführung | |
| Do 05.05. | V1 | [AA] Abstrakte Syntax, Einfach getypter λ-Kalkül | |
| U | Lambda-Interpreter | ||
| Di 10.05. | V2 | [AA] Operationale Semantik, Grund- und Datentypen | |
| Do 12.05. | V1 | [AA] Curry-Howard | |
| U | Erweiterter Interpreter | ||
| Di 17.05. | V2 | [US] Typinferenz, Substitutionen, Unifikatoren | |
| Do 19.05. | V1 | [US] Allgemeinster Unifikator, Unifikation | |
| U | Typinferenz | Typinferenz in Haskell | |
| Di 24.05. | V2 |
[US] Effiziente Unifikation (mittels union-find) |
Unifikation mit union find in OCaml |
| Do 26.05. | V1 | [US] ML Polymorphismus | |
| U | Unifikation | ||
| Di 31.05. | V2 | [US] System F, Imprädikative Datentyp-Kodierungen | |
| Do 02.06. | Christi Himmelfahrt | ||
| Di 07.06. | V2 | [US] Parametrizität, Theorems for free | |
| Do 09.06. | V1 | [US] Adäquatheit von Datentyp-Kodierungen | |
| U | Polymorphismus | ||
| Di 14.06. | Pfingsten | ||
| Do 16.06. | V1 | [AA] Referenzen | |
| U | Referenzen | ||
| Di 21.06. | V2 | [AA] Effekttypen | |
| Do 23.06. | Fronleichnam | ||
| Di 28.06. | V2 | [AA] Subtyping | |
| Do 30.06. | V1 | [AA] Subtyping | |
| U | Subtyping | ||
| Di 05.07. | V2 | [AA] Rekursive Typen | |
| Do 07.07. | V1 | [AA] Koinduktion | |
| U | Rekursive Typen | ||
| Di 12.07. | V2 | [US] Objekte, Featherweight Java | |
| Do 14.07. | V1 | [US] Generic FJ | |
| U | Objektorientierung | ||
| Di 19.07. | V2 | [AA] Abhängige Typen | |
| Do 21.07. | V1 | [AA] Abhängige Typen | |
| U | Agda | ||
| Di 26.07. | V2 | [RG] Sicherheitstypsysteme | |
| Do 28.07. | Prüfung |
Literatur
- Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002
Weiterführende Informationen
- Mitchell Wand. A Simple Algorithm and Proof for Type Inference. Fundamenta Infomaticae, 10, 1987.
- Franz Baader, Wayne Snyder. Unification Theory, Handbook of Automated Reasoning, Elsevier, 2001
- Didier Remy. Using, Understanding, and Unraveling the OCaml Language, 2001
- Jean-Yves Girard, Yves Lafont, Paul Taylor. Proofs and Types, 1989
Artikelaktionen