Theorie der Programmierung (SoSe 2020)

Die Veranstaltung findet bis zur Wiederaufnahme der Präsenzlehre online statt. Um laufende Informationen, insbesondere Links zu Zoom-Sitzungen (o.ä.), zu erhalten, treten sie idealerweise dem StudOn-Kurs bei.

  • Die Zoom-Sitzungen werden als Online-Vorlesung abgehalten; sich hieraus ergebende Materialien, insbesondere Aufnahmen und den “Tafelanschrieb”, finden Sie auf StudOn
  • Es wird von einer vorherigen Vorbereitung seitens der Studierenden ausgegangen, anhand
    • der Videoaufnahme der vorigen Ausgabe der Veranstaltung und
    • des weiter unten verlinkten Veranstaltungsskripts.
  • Wir geben an dieser Stelle fortlaufend den geplanten Inhalt der jeweils nächsten Sitzung bekannt:
    • Mo. 20.04.2020: Folge 1 der Videoaufzeichnung, Skript Abschnitt 1 und Anfang von Abschnitt 2 bis exklusive Unterabschnitt 2.1.
    • Di. 21.04.2020: Folge 2 der Videoaufzeichnung, Skript Abschnitt 2.1.1 (Binäre Relationen)
    • Mo. 27.04.2020: Folge 3 der Videoaufzeichnung, Skript Abschnitte 2.1.2 und 2.1.3 (Terme, Grundbegriffe von Termersetzungssystemen)
    • Di. 28.04.2020: Folge 4 der Videoaufzeichnung, Skript Abschnitt 2.2 bis einschließlich Abschnitt 2.2.1 (Reduktionsordnungen).
    • Mo. 04.05.2020: Rest von Folge 4 und Folge 5 der Videoaufzeichnung, Skript Abschnitt 2.2.2 (Polynomordnungen).
    • Di. 05.05.2020: Folge 6 der Videoaufzeichnung, Skript Abschnitt 2.3 (Konfluenz) bis Satz 2.50.
    • Mo. 11.05.2020: Folge 6 der Videoaufzeichnung, Skript bis Beispiel 2.61 (Kritische Paare)
    • Di. 12.05.2020: Folge 7 der Videoaufzeichnung, Skript Rest Abschnitt 2 (Critical Pair Lemma, wohlfundierte Induktion, Newman’s Lemma)
    • Mo. 18.05.2020: Folge 8 der Videoaufzeichnung, Skript bis Abschnitt 3.1.1 (lambda-Kalkül, beta-Reduktion)
    • Di. 19.05.2020: Folge 9 der Videoaufzeichnung, Skript Abschnitt 3.1.2 (Rekursion), 3.1.3 (Auswertungsstrategien) bis ca. Bemerkung 3.15
    • Mo. 25.05.2020: Folge 9 und Folge 11 der Videoaufzeichnung, Skript Abschnitt 3.1.3 (Nachtrag zu Auswertungsstrategien) und 3.2.1 (einfach getypter lambda-Kalkül)
    • Di. 26.05.2020: Folge 12 der Videoaufzeichnung, Skript Abschnitt 3.2.2 (Typinferenz)
    • Mo. 08.06.2020: Folge 13 der Videoaufzeichnung, Skript Rest Abschnitt 3.2.2 (Korrektheit der Typinferenz) und 3.2.3 (Subjektreduktion)
    • Di. 09.06.2020: Folge 14 der Videoaufzeichnung, Skript Abschnitt 3.2.5 (Church-Rosser)
    • Mo. 15.06.2020: Folge 15 der Videoaufzeichnung, Skript Abschnitt 3.2.4 (Curry-Howard-Isomorphismus), 4 (Datentypen) bis ca. Def. 4.4 (Homomorphismen)
    • Di. 16.06.2020: Folge 16 der Videoaufzeichnung, weiter Skript Abschnitt 4 (Datentypen) bis ca. Lemma 4.13 (Mengenkonstruktionen)
    • Mo. 22.06.2020: Rest von Folge 16 sowie Folge 17 der Videoaufzeichnung, Skript Abschnitt 4.1 (Initialität und Rekursion)
    • Mo. 29.06.2020: Rest von Folge 17 sowie Folge 18 der Videoaufzeichnung, Skript Abschnitt 4.2 (mehrsortige Datentypen)
    • Mo. 06.07.2020: Folge 20 der Videoaufzeichnung, Skript Abschnitt 4.5 (Korekursion)
    • Di. 07.07.2020:  Rest Folge 20 sowie Folge 21 der Videoaufzeichnung, Skript Abschnitte 4.6 (Koinduktion),, 4.7 (Kodatentypen mit mehreren Nachfolgerfunktionen), evtl. schon Anfang Abschnitt 5 (Polymorphie)
    • Mo. 13.07.2020: Erste Hälfte von  Folge 22 der Videoaufzeichnung, Skript Abschnitt 5.1 (Datentypen in System F) und Folge 22 der Aufzeichnung von 2018, Skript Abschnitt 5.3 (ML-Polymorphie)
    • Di. 14.07.2020: Fortsetzung ML-Polymorphie.
    • Mo. 20.07.2020: Rest Folge 22, Skript Abschnitt 6.1/6.2 (Automaten und Sprachen), sowie eventuell Anfang von Folge 23 der Videoaufzeichnung, Skript Abschnitt 6.3 (Automaten als Kodaten)
    • Di. 21.07.2020: Rest Folge 23 der Videoaufzeichnung, Skript Abschnitt 6.4 (Automatenminimierung).
    • Mo. 27.07.2020: Folge 24 der Videoaufzeichnung, Skript Abschnitt 5.4 (Starke Normalisierung in System F)

Klausur

Zur Klausur sind sämtliche papierbasierten Hilfsmittel zugelassen. Wir empfehlen einen rechtzeitigen Blick auf die Probeklausur. (Die aber natürlich unverbindlichen Charakter hat, insbesondere garantieren wir nicht, dass alle Aufgabentypen aus der Probeklausur auch in der tatsächlichen Klausur vorkommen.)

Bitte beachten sie ferner die Hygieneregelungen.

Termine

Sämtliche Termine müssen als vorläufig angesehen werden

Vorlesungen

Mo, 16:15 – 17:45, H9; Di, 12:15 – 13:45, H9

Termin Zeit Ort Dozent Beginn
Mo. 16:15 – 17:45 H9 Lutz Schröder 20.4.
Di. 12:14 – 13:45 H9 ::: :::

Intensivübung

Fr, 14:15 – 15:45, H4

Termin Zeit Ort Dozent Beginn
Fr. 14:15 – 15:45 H4 Paul Wild 1.5.

Tutorien

Die Anmeldung zu den Tutorien erfolgt in der ersten Semesterwoche über mein Campus. Beginn der Übungen ist in der zweiten Vorlesungswoche (ab 27. April).

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.

Vorläufig: 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

Skript

Es gibt ein auf einer studentischen Mitschrift vom SoSe 2014 basierendes Skript (Stand 07.10.20), 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