Theorie der Programmierung (SS 2017)

Termine

Wiederholungsklausur

Die Wiederholungsklausur fand am 19. Februar im H9 statt. Die Klausureinsicht ist am Mittwoch, den 28. Februar um 14 Uhr in Raum 11.150-113.

Klausur

<fc #FF0000>Fragestunde:</fc> Wir bieten am Freitag, den 6. Oktober um 15 Uhr in Raum 00.131-128 eine Fragestunde für die Klausur an.

<fc #FF0000>Klausur:</fc> Das Datum der Klausur kann mittlerweile in mein campus eingesehen werden. Zur Klausur sind sämtliche papierbasierten Hilfsmittel zugelassen. Die Bonuspunkte sind in Waffel eingetragen. Wir empfehlen einen rechtzeitigen Blick auf die

<fc #FF0000>Klausurergebnisse:</fc> Die Klausur ist korrigiert und die Ergebnisse in mein Campus einsehbar. Die Einsicht findet am Donnerstag, den 26.10.2017 um 15:30 Uhr in Raum 11.150-113 statt.

<WRAP half column> Notenverteilung:

</WRAP>

<WRAP half column> Statistik:

Teilnehmer 112
Bestanden 78.6%
Durchschnitt 3.0

</WRAP>

Vorlesungen

Termin Zeit Ort Dozent Beginn
Mo. 14:15 – 15:45 C1 – Chemikum Lutz Schröder 24.4.
Do. 16:15 – 17:45 H9 ::: :::

Intensivübung

<!– <fc #FF0000>Achtung!</fc> Am Freitag, den 26. Mai, findet keine Intensivübung statt. Bei Bedarf kann ein Ersatztermin gefunden werden, bitte dazu Mail an Christoph Rauch.–>

Termin Zeit Ort Dozent Beginn
Fr. 14:15 – 15:45 0.68 Christoph Rauch

Tutorien

Die Anmeldung zu den Tutorien erfolgt über Waffel. Die verfügbaren Termine sind der untenstehenden Tabelle zu entnehmen (die von den Angaben in UnivIS abweichen kann). Beginn der Übungen ist in der zweiten Vorlesungswoche.

<!– <fc #FF0000>Achtung!</fc> Aufgrund des Ansturms auf die Tutorien von Montag bis Donnerstag haben wir noch zwei Tutorien jeweils am Dienstag, 12:00–14:00 Uhr, sowie am Donnerstag, 12:00–14:00 Uhr, eingerichtet. Diese werden jeweils am Freitag den Termin von 8:00–12:00, und einen der Termine von 16:00–18:00 Uhr, ersetzen. Wir bitten allerdings die Teilnehmer, die sich bereits für Freitag 16:00–18:00 eingeschrieben haben, auch in dieser Gruppe zu verbleiben! –> <fc #FF0000>Achtung!</fc> In den Wochen vom 5. bis 9. Juni sowie vom 12. bis 16. Juni wird in den Übungen derselbe Stoff behandelt. Es ist also nicht nötig, in diesen beiden Wochen eine andere Übungsgruppe zu besuchen, falls die eigene Übung ausfällt. Der Bergdienstag ist selbstverständlich frei. Ebenfalls entfällt die Freitagsübung am 16. Juni. <!– <fc #FF0000>Achtung!</fc> Donnerstag, der 25. Mai, ist ein Feiertag. Wir bitten die Teilnehmer der Donnerstagstutorien, ausnahmsweise eine andere Übung zu besuchen. Die Freitagsübung am 26. Mai findet mangels Teilnehmer in dieser Woche auch nicht statt! Falls es noch zusätzlich Nachholbedarf gibt, wird auf Rückfrage nächste Woche noch eine zusätzliche Übung angeboten. –>

<fc #FF0000>Verteilung der Bonuspunkte:</fc> 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.

Termin Zeit Ort Dozent
Mo. 16:15 – 17:45 0.68 Johannes Kern
Di. 10:15 – 11:45 00.131-128 Florian Unger
Di. 12:15 – 13:45 02.134-113 Kevin Höllring
Di. 12:15 – 13:45 00.131-128 Frederik Haselmeier
Do. 12:15 – 13:45 0.85 Kristin Braun
Do. 12:15 – 13:45 01.151-128 Üsame Cengiz
Do. 12:15 – 13:45 00.131-128 Kevin Höllring
Fr. 16:15 – 17:45 01.151-128 Simone Weiß

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.

  • (rev. 16342 16353). Abgabe: 08.05. — 12.05.
  • (rev. 16426). Abgabe: 15.05. — 19.05.
  • (rev. 16592). Abgabe: 22.05. — 26.05.
  • (rev. 16782). Abgabe: 29.05. — 02.06.
  • (rev. 16849). Abgabe: 08.06. — 13.06.
  • (rev. 16899). Abgabe: 19.06. — 23.06.
  • (rev. 17046 17122). Abgabe: 26.06. — 30.06.
  • (rev.17146). Abgabe: 03.07. — 07.07.
  • (rev. 17255 17353). Abgabe: 10.07. — 14.07.
  • (rev. 17402). Abgabe: 17.07. — 21.07.
  • (rev. 12854). Abgabe: 24.07. — 28.07.
  • (rev. 17549).

<!– <fc #FF0000>Verteilung der Bonuspunkte:</fc> 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.

  • (rev. 12966).

–>

Inhalt

Themen

  • Termersetzung
  • λ-Kalkül
  • Semantik von Programmiersprachen, Bereichstheorie
  • Induktion und Koinduktion
  • Reguläre Sprachen und endliche Automaten
  • Stichpunktartige

Skript

Es gibt ein auf einer studentischen Mitschrift vom SoSe 2014 basierendes, vorläufig noch inoffizielles

  • [Revision 18112],

das im Laufe der Veranstaltung überarbeitet wird (siehe Revisionsnummern).

<!–

Zusatzmaterial der Tutoren (ohne Gewähr)

  • Folien zu den Tutorien
    • (Termersetzung)
    • (Termersetzung: Termination)
    • (Termersetzung: Konfluenz)
    • (λ-Kalkül: Reduktion, Church-Kodierung)
    • (λ-Kalkül: Rekursion, Typinferenz)
    • (λ-Kalkül: Curry-Howard Isomorphismus; Induktive Datentypen: Definition von Funktionen)
    • (λ-Kalkül: Subjektexpansion; Induktive Datentypen: Folds)
    • (Induktive Datentypen: Induktionsbeweise)
    • (Koinduktive Prozesstypen: Definition von Funktionen, Bisimulationsbeweise)
    • (Koinduktive Prozesstypen: Exponentiation, Kodatentypen mit Alternativen)
    • (System F: Kodierung von Datentypen, Typinferenz)
    • (Reguläre Ausdrücke, Pumping Lemma, endliche Automaten)

–>

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
  • 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