19567

WiSe 12/13: Seminar Typ- und Effektsysteme

Marcel Kyas

Additional information / Pre-requisites

2,4

Comments

Inhalt Ein Typ- und Effektsystem ist eine syntaktische Methode zum Beweisen der Abwesenheit von bestimmten Fehlern in Programmen, die das Programmverhalten entsprechend der Art der Werte klassifiziert, die ein Programm generiert. Übersetzer mit Typ- und Effektsysteme sowie das Studium der typtheoretsichen Eigenschaften von Programmiersprachen haben heute wichtige Anwendung in der Softwaretechnik, dem Entwurf von Programmiersprachen, von Hochleistungsübersetzern, und der Daten- und Informationssicherheit.In diesem Seminar wird in die Grundlagen von Typ- und Effektsystemen und ihrer metatheoretischen Eigenschaften eingeführt. Dazu gehören die Parallelen zwischen Typsystemen und Logiken sowie Typrekonstruktion und Beweissuche. Über diese Grundlagen hinaus werden Standardanwendungen von Typsystemen in der Programmierung sowie Nichtstandardanwendungen in derDaten- und Informationssicherheit, nichtsequentiellen Programmierung,Speicher- und Programmablaufplanung und weiteren.Kerninhalte sind der ungetyüte und einfachgetypte Lambdakalkül, Typrekonstruktion und Typüberprüfung, universeller und existentieller Polymorphismus, Untertypen, beschränkte Quantifizierung, rekursive Typen, kinds und Typoperatoren sowie die Anwendung dieser Konzepte in funktionalen und objektorientierten Programmiersprachen, dem Entwurf von sicheren und zuverlässigen Systemen, sowie von nichtsequentiellen und eingebetteten Systemen. Zielgruppe Studierende im dritten Studienjahr des Bachelorstudiengangs und des Masterstudiengangs Informatik. Voraussetzungen Mathematik für Informatiker I, Grundlagen der theoretischen Informatik und Semantik von Programmiersprachen wird sehr empfohlen, ist aber nicht notwendig. Literatur - Benjamin P. Pierce. Types and Programming Languages. The MIT Press, 2002 close