Proglang

Seminar: Type Systems

Leitung:Prof. Dr. Peter Thiemann
Mitwirkung:Annette Bieniusa
Zeit und Ort:
Di,14 - 16 in Geb. 101, Raum 01-018

Beschreibung

Typsysteme sind ein wichtiger Bestandteil moderner Programmiersprachen. Sie garantieren gewisse Sicherheitsaspekte von Programmen, können bei diversen Optimierung helfen und dienen auch der Dokumentation.

In den ersten Wochen des Seminars werden die notwendingen Grundlagen durch die Lektüre und gemeinsame Diskussion ausgewählter Kapitel aus "Types and Programming Languages" (siehe Material) erworben. In späteren Seminarsitzungen stellen dann die Teilnehmer ihre erarbeiteten Themen vor.

Prüfungsleistung

In einem Seminar werden in erster Linie Fachkenntnisse vertieft, aber auch Kompetenzen vermittelt, die eine notwendige Grundlage für eine wissenschaftliche Arbeitsweise sind. Dazu gehören:

Zeitplan

In den ersten Sitzungen werden wir folgende Abschnitte aus Types and Programming Languages von Benjamin C. Pierce besprechen:

DatumThemaMaterial
28.10.08Grundlagen, ungetypte arithmetische AusdrückeS. 1-44
04.11.08Ungetypter Lambda-Kalkül, TermeS. 51-82
11.11.08Getypte arithmetische Ausdrücke und getypter Lambda-KalkülS. 89-112
18.11.08Erweiterungen, NormalisierungS. 117-152
25.11.08SubtypingS. 179-220
02.12.08Polymorphismus: Universal typesS. 339-362

In der Sitzung am 2.12.2008 werden die Vortragsthemen verteilt. Die Vorträge der Seminarteilnehmer werden im Januar/Februar stattfinden.

Ausarbeitung

Die Ausarbeitung soll 10-15 Seiten umfassen. Sie muss mit

LaTeX, Dokumentklasse article und einer Schriftgröße von 11 Punkten

erstellt werden.

Themen

ThemaStudentBetreuer
Dependent Types [Pie05a]Olena BarthAnnette Bieniusa
Regular Expression Types [HVP00,HVP04]Steffen WittmerPhillip Heidegger
Typed Assembly Language [MWCG98,MWCG99]Christian SimonStefan Wehr
Linear Types [Pie05b]Benus BeckerProf. Dr. Peter Thiemann

Die Referenzen beziehen sich auf diese Literaturquellen.

Material

Das Seminar wird zunächst Teile des Buches "Types and Programming Languages von Benjamin C. Pierce besprechen. Es ist in der Fakultätsbibliothek verfügbar. Darüberhinaus sollen aktuelle Publikationen auf dem Gebiet der Typtheorie vorgestellt werden.