Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2011 / Typsysteme


Inhaltsbereich

Typsysteme

Vorlesung, 3-std., Abel, Schöpp; Übungen 2-std., Abel

 


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

 


Weiterführende Informationen

 

Artikelaktionen


Funktionsleiste