EN | DE
Theoretische Informatik

Theorie der Programmierung (SoSe2015)

Klausur

Das Datum der Klausur kann mittlerweile in mein campus eingesehen werden. Zur Klausur sind sämtliche papierbasierten Hilfsmittel zugelassen. Wir empfehlen einen rechtzeitigen Blick auf die

Übungsblätter

  • Übungsblatt 1 (rev. 8357). Abgabe: 11.05. – 15.05.
  • Übungsblatt 2 (rev. 8703). Abgabe: 01.06. – 05.06.
  • Übungsblatt 3 (rev. 8886 8936 8950 8971 9002). Abgabe: 06.07. – 10.07. Achtung, korrigierte Formulierung von Übungen 11 und 12 und neue Abgabefrist!
  • Übungsblatt 4 (rev. 8927). Abgabe: 06.07. – 10.07.
  • Übungsblatt 5 (rev. 9094). Abgabe: 13.07. – 17.07.

Termine

Vorlesungen

Termin Zeit Ort Dozent Beginn
Mo. 14:15 - 15:45 H4 Lutz Schröder 13.04.
Do. 14:15 - 15:45 H4

Intensivübung

Termin Zeit Ort Dozent Beginn
Fr. 10:15 - 11:45 H14 Daniel Hausmann 24.04.

Tutorien

Termin Zeit Ort Dozent Beginn
Mi. 12:15 - 13:45 E1.11 Christian Bay 22.04.
Do. 1 08:15 - 09:45 00.152-113 Ludwig Dietel 23.04.
Do. 2 08:15 - 09:45 00.151-115 Paul Wild 23.04.
Fr. 1 08:15 - 09:45 00.152-113 Ludwig Dietel 24.04.
Fr. 2 08:15 - 09:45 01.255-128 Ulrich Rabenstein 24.04.
Fr. 3 12:15 - 13:45 02.133-113 Daniel Hausmann 24.04.

Inhalt

Themen

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

Video-Aufzeichnung

Die Vorlesung wird vom RRZE aufgezeichnet und ist auf der RRZE-Seite zu finden.

Skript

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

  • Skript [Revision 8627 8772 8913 9059 9062 9126 9169 9433]

Zusatzmaterial der Tutoren (ohne Gewähr)

  • Folien zu den Tutorien
    • Übung 1 (Termersetzung: Terminierung)
    • Übung 2 (Termersetzung: Konfluenz)
    • Übung 3 (λ-Kalkül: Reduktion, Church-Kodierung)
    • Übung 4 (λ-Kalkül: Church-Kodierung, Rekursion)
    • Übung 5 (λ-Kalkül, getypt)
    • Übung 6 (Induktive Datentypen: Definition von Funktionen)
    • Übung 7 (Induktive Datentypen: Induktionsbeweise)
    • Übung 8 (Induktive Datentypen: Mehrsortigkeit; Koinduktive Prozesstypen: Definition von Funktionen)
    • Übung 9 (Koinduktive Prozesstypen: Koinduktionsbeweise, Kodatentypen mit Alternativen)
    • Übung 10 (System F: Kodierung von Datentypen, Typinferenz)
    • Übung 11 (Reguläre Ausdrücke, Pumping Lemma, endliche Automaten)
  • LaTeX-Vorlagen (als Hilfe zum Erstellen der Lösungen; Verwendung freiwillig):
    • Template: ueb_template.tex (PDF)
    • Beispielaufgabe: blatt1.tex
    • Die einzelnen Blätter werden in ueb_template.tex eingebunden und mittels pdflatex ueb_template kompiliert.
      Für mehr Informationen bitte die Kommentare in den .tex-Dateien lesen!
    • Nützliche Links:

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
  • J. Rutten: Automata and Coinduction - an exercise in coalgebra
  • A. Pitts: Lecture Notes on Regular Languages and Finite Automata, Cambridge University, 2013