M1102-DSE28-2020
Foundations of Certified Programming Languages and Compiler Design
|
|
| Modulverantwortlich: |
Prof. Dr.-Ing. Jerónimo Castrillón Mazo |
| Anzeige im Stundenplan: |
INF-DSE-20-E-CPLCD |
| Dauer: |
3 |
| Anzahl Wahlkurse: |
0 |
| Credits: |
6,0
|
| Startsemester: |
WiSe 2021/22 |
| Verantwortliche:r Dozent:in |
Prof. Castrillon
jeronimo.castrillon@mailbox.tu-dresden.de |
| Qualifikationsziele |
Nach dem erfolgreichen Abschluss dieses Moduls sind die Teilnehmenden in der Lage, Programme mit starker Garantie über deren Eigenschaften zu entwickeln, um den Testaufwand zu minimieren und komplexe Laufzeitfehler 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 Agda oder Theorem Provern wie Coq zu entwickeln
und deren Eigenschaften formal zu beweisen. Die Teilnehmenden
kennen wesentliche Beweisverfahren, um Eigenschaften von Programmiersprachen,
Compilern und sogar hardwarenahen Programmen
formal zu verifizieren. |
| Inhalte |
Das Modul vermittelt die Theorien des ungetypten und getypten Lambda-
Kalküls, sowie von Typsystemen mit Dependent Types und deren Verbindung
zur Aussagen- und Prädikatenlogik als Grundlage für den Curry-Howard-
Isomorphismus. Das Modul beinhaltet im Übrigen die Programmierung
mit stark-getypten Programmiersprachen, wie bspw. Agda, und Theorem
Provern, wie bspw. Coq. Auf dieser Grundlage wird auf Eigenschaften
von Programmiersprachen und Compilern und die Möglichkeiten,
diese im Designprozess von selbigen formal zu beweisen, eingegangen.
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 Kenntnisse und Fähigkeiten über die Grundlagen der Programmierung
und Logik auf Bachelorniveau vorausgesetzt. |
| Verwendbarkeit |
Das Modul ist ein Wahlpflichtmodul der fachlichen Vertiefung im Masterstudiengang
Distributed Systems Engineering. |
| Voraussetzungen für Vergabe von Leistungspunkten |
Die Leistungspunkte werden erworben, wenn die Modulprüfung bestanden
ist. Die Modulprüfung besteht aus einer mündlichen Prüfungsleistung
von 30 Minuten Dauer. |
| 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 Modulhandbuch TU Dresden |
INF-DSE-20-E-CPLCD |
