Theorie der Programmierung (SoSe 2019)
Klausur
Zur Klausur sind sämtliche papierbasierten Hilfsmittel zugelassen. Wir empfehlen einen rechtzeitigen Blick auf die
- Probeklausur (2019-07-30) Achtung: Aufgabe 2 wurde an den Stoff der ThProg-Ausgabe dieses Semesters angepasst.
2019-09-19: Am Mittwoch, den 25.09.2019 findet um 12:00 Uhr in Raum 00.131-128 eine Fragestunde zur Klausur statt.
Klausurergebnisse:Die Klausur ist korrigiert und die vorläufigen Ergebnisse in mein Campus einsehbar. Die Einsicht findet am Montag, den 28.10.2019 um 14:00 Uhr in Raum 11.150-113 statt.
Termine
Vorlesungen
Achtung: Zeiten geändert!
| Termin | Zeit | Ort | Dozent | Beginn |
|---|---|---|---|---|
| Mo. | 12:00 – 13:30 | H9 | Lutz Schröder | 25.4. |
| Do. | 12:00 – 13:30 | H9 | ::: | ::: |
Intensivübung
| Termin | Zeit | Ort | Dozent | Beginn |
|---|---|---|---|---|
| Do. | 16:15 – 17:45 | H4 | Christoph Rauch | 2.5. |
Tutorien
Die Anmeldung zu den Tutorien erfolgt in der ersten Semesterwoche über mein Campus. Beginn der Übungen ist in der zweiten Vorlesungswoche (ab 29. April).
Verteilung der Bonuspunkte: Bonuspunkte erhält, wer mindestens 50% der Punkte in den Hausaufgaben erreicht hat. Die maximale Anzahl an Bonuspunkten (also 6) gibt es bei 90% der Punkte oder mehr, dazwischen wird linear skaliert. Bonuspunkte können wie immer nicht zum Bestehen der Klausur führen, sondern lediglich zur Verbesserung der Note bei bestandener Klausur.
Die Abgabe der Übungen erfolgt wöchentlich in Gruppen von 2 bis 3 Personen.
Übungsblätter
Die Blätter enthalten Präsenzaufgaben für die Tutorien und bepunktete Hausaufgaben, die zum Erwerb von Bonuspunkten für die Klausur abgegeben und korrigiert werden. Die Übungsblätter werden auf einer separaten Übungshomepage veröffentlicht.
Inhalt
Themen
- Termersetzung
- λ-Kalkül
- Semantik von Programmiersprachen, Bereichstheorie
- Induktion und Koinduktion
- Reguläre Sprachen und endliche Automaten
- Stichpunktartige topics.pdf
Skript
Es gibt ein auf einer studentischen Mitschrift vom SoSe 2014 basierendes
das im Laufe der Veranstaltung überarbeitet wird (siehe Revisionsnummern). Der Inhalt des Skripts ist während der Vorlesungszeit stets als vorläufig anzusehen, insbesondere hinsichtlich des Umfangs des Materials; will sagen, es kann ggf. Material hinzukommen. Eine Version, die dem tatsächlichen Ablauf der Veranstaltung entspricht, wird erst nach Abschluss der Vorlesungen zur Verfügung gestellt.
Literatur
- F. Baader, T. Nipkow: Term rewriting and all that, Cambridge University Press, 1999
- J.-W. Klop, Term rewriting systems, in S. Abramsky, D. Gabbay and T. Maibaum (eds.), Handbook of Logic in Computer Science, Oxford University Press, 1992
- J. Giesl, Termersetzungssysteme, RWTH Aachen, 2011
- H. Barendregt, λ-calculi with types, in S. Abramsky, D. Gabbay and T. Maibaum (eds.), Handbook of Logic in Computer Science, Oxford University Press, 1992
- T. Nipkow, Lambda-Kalkül, TU München, 2004
- W. Richter, A proof of the standard reduction theorem in the lambda calculus
- M. Felleisen, Programming Languages and Lambda Calculi, 1998
- G. Winskel, Formal Semantics of Programming Languages, MIT Press, 1993
- J. E. Hopcroft, J. D. Ullman and R. Motwani, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Prentice Hall, 2006
- B. Jacobs, J. Rutten: A Tutorial on (Co-)Algebras and (Co-)Induction, EATCS Bulletin 42 (1997), 222-259.
- J. Rutten: Automata and Coinduction (an exercise in coalgebra), Proc. CONCUR’98, LNCS 1466, 194-218, Springer, 2006.
- P. Taylor: Proofs and Types, Cambridge University, 2003
- M. H. B. Sørensen, P. Urzyczyn: Lectures on the Curry-Howard Isomorphism, 1998
- A. Pitts: Lecture Notes on Regular Languages and Finite Automata, Cambridge University, 2013