Foundations of Certified Programming Language and Compiler Design
Überblick
Qualifikationsziele:
Nach dem erfolgreichen Abschluss dieses Moduls sind die Teilnehmenden in der Lage, Programme mit starken Garantie über deren Eigenschaften zu entwicklen, um den Testaufwand zu minimieren und komplexe Laufzeitfehler schon während des Entwicklungsprozesses zu vermeiden. Dazu kennen die Teilnehmenden die Grundlagen von stark-getypten Programmiersprachen (dependently-typed languages) und deren Verbindung zur Logik. Dieses Wissen ermöglicht es den Teilnehmenden Programme in Programmiersprachen wie Haskell oder Theorem Provern wie Coq zu entwicklen und deren Eigenschaften formal zu beweisen. Die Teilnehmenden kennen wesentliche Beweisverfahren, um Eigenschaften von Programmiersprachen, Compilern und sogar Hardware-nahen Programmen formal zu verifizieren.
Inhalte:
Das Modul vermittelt die Theorien des ungetypten und getypten Lambda-Kalküls, Typsystemen mit Dependent Types und deren Verbindung zur Aussagen- und Prädikatenlogik als Grundlage für den Curry-Howard-Isomorphismus. Um den Teilnehmenden diese Theorie auch praktisch näher zu bringen, beinhaltet dieses Modul die Programmierung mit stark-getypten Programmiersprachen (Haskell) und Theorem Provern (Coq). Darauf basierend wird auf Eigenschaften von Programmiersprachen und Compilern eingegangen, die es gilt im Designprozess von selbigen formal zu beweisen. Dazu werden wichtige Beweistechniken eingeführt und die formalen Konzepte zur Beschreibung der verschiedenen semantischen Definitionen (operationell, denotationell) vermittelt.
Lehr- und Lernformen:
Das Modul umfasst Vorlesungen im Umfang von 2 SWS und Übungen im Umfang von 2 SWS sowie Selbststudium.
Voraussetzungen für die Teilnahme:
Es werden die im Grundstudium erworbenen Kenntnisse und Kompetenzen in den Fächern Programmierung und Logik vorausgesetzt.
Voraussetzungen für die Vergabe von Leistungspunkten:
Die Leistungspunkte werden erworben, wenn die Modulprüfung bestanden ist. Die Modulprüfung besteht aus einer mündlichen Prüfungsleistung im Umfang von 30 Minuten.
Leistungspunkte und Noten:
Durch das Modul können 6 Leistungspunkte erworben werden. Die Modulnote entspricht der Note der Prüfungsleistung.
Häufigkeit des Moduls:
Das Modul wird jedes Wintersemester angeboten.
Arbeitsaufwand:
Der Arbeitsaufwand beträgt 180 Stunden.
Dauer des Moduls:
Das Modul erstreckt sich über ein Semester.
Modulnummer:
INF-DSE-20-E- FCPLCD
NES-INF-E-FCPL
Dozent und verantwortlicher Hochschullehrer an der TUD:
