Inhalt
Die formale Semantik einer Programmiersprache legt mit mathematischen Methoden die exakte Bedeutung eines Programms bzw. seines Ablaufs fest. Nicht nur verbessert eine formale Semantik Verständnis und Präzision von Sprachen und ihren Beschreibungen; formale Semantik ermöglicht erst den strengen Beweis von Sicherheitseigenschaften, wie z.B. dass ein Programm nicht wegen illegaler Casts abstürzen kann ("Typsicherheit"). Die Veranstaltung stellt Grundlagen und Anwendungen moderner Semantik vor.
Themen:
- Abstrakte Syntax
- Typsysteme
- Denotationale Semantik
- Continuation-Semantik
- Operationale Semantik
- Typsicherheit
- Korrektheit der Hoare-Logik
- aktuelle Entwicklungen
Lernziele
Kenntnis der Grundlagen und Anwendungen von operationaler und denotationaler Semantik; Einblick in aktuelle Forschung
