WS 2006/07: Theorie der Programmierung I + II

Termine

Vorlesung Di 12:15 - 13:45 H-F 104/05

Do 14:15 - 15:45 H-F 116
Erste Vorlesung Di 17.10.2006
Übungen Mi 12:15 - 13:45 H-A 8118/19

Fr 12:15 - 13:45 H-A 6118/19
Erste Übung Mi 18.10.2006 bzw. Fr 20.10.2006
Sprechstunde Di 14:00 - 15:00 H-A 8113

Aufteilung

Teil I der Vorlesung endet kurz vor Weihnachten, Teil II schließt sich unmittelbar an.

Leitfaden zur Prüfungsvorbereitung

PDF

Übungsblätter

Übung 1 PDF
Übung 2 PDF
Übung 3 PDF
Übung 4 PDF
Übung 5 PDF
Übung 6 PDF
Übung 7 PDF
Übung 7 (erweitert) PDF
Übung 8 (korrigiert) PDF
Übung 9 PDF
Übung 10 PDF
Übung 11 PDF
Übung 12 PDF

Lösungen

O'Caml-Lösung zu Übung 4, Aufgabe 3
Java-Lösung zu Übung 4, Aufgabe 3 als Eclipse Projekt, siehe README
O'Caml-Lösung zu Übung 6, Aufgabe 5
O'Caml-Lösung zu Übung 9, Aufgabe 2
O'Caml-Lösung zu Übung 10, Aufgabe 1
O'Caml-Lösung zu Übung 11, Aufgabe 3
O'Caml-Lösung zu Übung 12, Aufgabe 3

TPML:

TPML ist ein spezielles Lernwerkzeug für die Vorlesung "Theorie der Programmierung", das in einer Projektgruppe entwickelt wird. Es bietet bisher als interaktive (schrittweise) Lernhilfe einen Small step Interpreter, Big step Interpreter und Type Checker für die (meisten der) in der Vorlesung betrachteten Programmiersprachen.

Nähere Informationen unter http://tinyurl.com/y6ov4u

Materialien aus der Vorlesung und den Übungen

Abstrakte Syntax der Sprachen L0 und L1 PDF
Folien aus der Einführungsübung (überarbeitet) PDF
Small step Semantik der Sprachen L0 und L1 PDF
Die einfach getypten Sprachen L0t, L1t, L2t PDF


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 in Teil I 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" 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, Cambridge University Press 1996

Das wohl bekannteste Lehrbuch über SML. Natürlich gibt's noch viele andere Bücher zum gleichen Thema.

6. Objective Caml

Leider gibt's (noch?) kein Lehrbuch zu O'Caml. Eine Fülle von Informationen findet man auf http://caml.inria.fr/ocaml/index.en.html
Kurt Sieber