WS 2004/05: Theorie der Programmierung I

Termine

Vorlesung Mi 12:15 - 13:45  H-F 104/5 
Erste Vorlesung  Mi 13. 10. 2004 
Übung  Mi 14:15 - 15:45  H-F 104/5 
Erste Übung  Mi 27. 10. 2004 



Folien aus der Vorlesung Ergänzungen

Vorlesung vom 13.10.2004   Stand: 13.10.2004   (Seiten 1-9)   PDF (66 K)
Vorlesung vom 20.10.2004   Stand: 21.10.2004   (Seiten 10-20)   PDF (62 K)  

Herleitung eines Typurteils:   PDF (19 K)
Vorlesung vom 27.10.2004   Stand: 28.10.2004   (Seiten 21-29)   PDF (29 K)  

Eine abgeleitete Regel:   PDF (29 K)
Vorlesung vom 03.11.2004   Stand: 10.11.2004   (Seiten 30-41)   PDF (91 K)  
Small step Semantik (vorläufige Version)   Stand: 24.11.2004   (Seiten 44-49)   PDF (54 K)  
Vorlesung vom 01.12.2004 (vorläufige Version)   Stand: 08.12.2004   (Seiten 48-57)   PDF (86 K)  
Herleitung eines polymorphen Typs Die Funktion map       PDF (30 K)

Übungsblätter

Übung 1 PDF
Übung 2 PDF
Übung 3 PDF
Übung 4 PDF
Übung 5 PDF
Übung 6 PDF
Übung 7 PDF
Übung 8 PDF

Lösungen

Übungsblatt 3, Aufgabe 1 a b d e f
Übungsblatt 4, Aufgabe 1 a b c d e f
Übungsblatt 5, Aufgabe 2 twice
Übungsblatt 6, Aufgabe 1 ggT
Übungsblatt 6, Aufgabe 2 b c d

Prüfungen

Hier finden Sie einen Leitfaden zur Prüfungsvorbereitung (aus dem WS 2003/04): PDF
Zur Vereinbarung eines Prüfungstermins können Sie mir eine e-mail schicken und/oder persönlich vorbeikommen.

Praxis

Wer die "Theorie der Programmierung" durch etwas "Praxis der Programmierung" ergänzen möchte, kann sich SML/NJ (= "Standard ML of New Jersey") besorgen. Das ist die real existierende Programmiersprache, an die sich die in der Vorlesung definierte Sprache anlehnt. Alle nötigen Informationen dazu gibt's auf der SML/NJ-Homepage


Literatur

1. Benjamin Pierce: Types and Programming Languages, MIT Press, 2002

In diesem Buch werden (nur) small-step Semantik und Typsysteme behandelt. Dabei wird in Teil II (Kapitel 8-14) etwa die gleiche Programmiersprache abgedeckt, die wir auch in der Vorlesung betrachten, und es werden ähnliche Resultate (z.B. Typsicherheit) für diese Sprache bewiesen. Insgesamt ist das Buch sehr als Vorlesungsbegleitung zu empfehlen.

2. Glynn Winskel: The Formal Semantics of Programming Languages, MIT Press, 1993

In Kapitel 2,5 und 6 des Buches werden operationelle, denotationelle und axiomatische Semantik für eine einfache imperative Sprache behandelt, in Kapitel 9, 10 und 11 werden Typsysteme, operationelle und denotationelle Semantik für funktionale Sprachen betrachtet. Der Schwerpunkt bei der operationellen Semantik liegt auf big-step, small-step kommt nur am Rande vor (Absatz 2.6).

3. Robin Milner, Mads Tofte and Robert Harper: The Definition of Standard ML, MIT Press 1990

In diesem Buch wird die funktionale Programmiersprache "Standard ML" (an die sich die in der Vorlesung definierte Sprache anlehnt) formal definiert, d.h.
- die Syntax (= kontextfreie Syntax) in Kapitel 1 und 2
- die statische Semantik (= Typregeln) in Kapitel 3 und 4
- die dynamische Semantik (= big step Semantik) in Kapitel 5 und 6
Man kann hier einmal sehen, wie die Techniken, die wir in der Vorlesung erlernen, auf eine echte Programmiersprache angewendet werden. Das ist natürlich sehr aufwendig.

4. Robin Milner and Mads Tofte: Commentary on Standard ML, MIT Press, 1991

Hier werden Erläuterungen zu 3. gegeben und es werden einige Sätze über die Semantik bewiesen.

5. Larry C. Paulson: ML for the working programmer

Sehr zu empfehlen für jeden, der in ML programmieren oder auch nur etwas mehr Gefühl für's funktionale Programmieren bekommen möchte (was ja für die Vorlesung nicht schaden kann!). Natürlich gibt's noch viele andere Bücher zum gleichen Thema.
Kurt Sieber