Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2010 / Semantik von Programmiersprachen


Inhaltsbereich

Semantik von Programmiersprachen

Vorlesung, 4-std., Mo 12-14, Mi 10-12; Übung 2-std., Do 16-18; Abel, Schöpp

 

 


Aktuelles

  • Die Prüfungen finden am 8. Oktober statt.
  • Die Übung am 22.7. findet im Raum L109 statt.

 


Inhalt

Bei der Arbeit mit Programmiersprachen, zum Beispiel bei der Entwicklung von Compilern und Interpretern oder bei der Programmanalyse, ist es wichtig, dass die Bedeutung von Programmen (ihre Semantik) genau festgelegt ist. In dieser Vorlesung sollen Grundlagen der Semantik von Programmiersprachen vermittelt werden. Neben der reinen Spezifikation der Bedeutung von Programmen soll auf einige der vielfältigen Anwendungen semantischer Methoden eingegangen werden, zum Beispiel in der rechnergestützten Analyse und Verifikation von Programmen oder in der Entwicklung von Typsystemen.

  1. Einführung in operationelle, denotationelle und axiomatische Semantik am Beispiel einer einfachen imperativen Sprache
  2. Lambda-Kalkül mit einfachen Typen
  3. Operationelle und denotationelle Semantik einer funktionalen Programmiersprache (PCF)
  4. Algorithmische Spielsemantik

 


Organisation

 


Zeit und Ort

Veranstaltung Zeit Ort Beginn
Vorlesung Mo, 12-14 Uhr Raum 065 (Oettingenstr. 67) 19.04.2010
Vorlesung Mi, 10-12 Uhr Raum 065 (Oettingenstr. 67) 21.04.2010
Übung Do, 16-18 Uhr Raum 065 (Oettingenstr. 67) 29.04.2010

 


Log

Termin Stoff Sonstiges
19.04. Einführung und Überblick  
21.04. Syntax von IMP, SMC-Maschine, strukturelle Induktion Übungsblatt 1
26.04. Induktive Definitionen, Regelinduktion  
28.04. Small-Step-Semantik für IMP Übungsblatt 2
03.05. Big-Step-Semantik für IMP, Einige Spracherweiterungen bigstep.hs, bigstep.ml
05.05. Denotationelle Semantik für IMP Übungsblatt 3
10.05. Grundbegriffe der Bereichstheorie  
12.05. Fortsetzung Bereichstheorie Übungsblatt 4
17.05. Axiomatische Semantik für IMP  
19.05. Lambda-Kalkül: Syntax, α-Äquivalenz Übungsblatt 5
26.05. β-Reduktion, lokale Konfluenz Übungsblatt 6
31.05. Konfluenz der beta-Reduktion  
02.06. Typzuweisung Übungsblatt 7
07.06. Getypte Gleicheit und Standardmodell  
09.06. Umgebungsmodelle Übungsblatt 8
14.06. Termmodelle und Normalisierung  
16.06. Logische Relationen und Vollständigkeit des Standardmodells Übungsblatt 9
21.06. Kategorien  
23.06. Kartesisch abgeschlossene Kategorien Übungsblatt 10
28.06. Lambda-Kalkül und CCCs  
30.06. Effekte im Lambda-Kalkül Übungsblatt 11
05.07. Effekte und Monaden  
07.07. PCF Syntax und Big-Step Semantik Übungsblatt  12 
12.07. PCF Observationsäquivalenz und Kontextlemma  
14.07. CPO-Semantik für PCF Übungsblatt  13
19.07. PCF Interpretation, Adäquatheit  
21.07. Adäquatheit, Full Abstraction  

 


Literatur

Bücher

Weitere Artikel

 

Artikelaktionen


Funktionsleiste