Vorlesungen
| Termin | Zeit | Ort | Dozent | Beginn |
|---|---|---|---|---|
| Mo. | 14:15 – 15:45 | H9 | Paul Wild | 13.04. |
| Fr. | 10:15 – 11:45 | H9 | Paul Wild | 17.04. |
Intensivübung
| Termin | Zeit | Ort | Dozent | Beginn |
|---|---|---|---|---|
| Do . | 16:15 – 17:45 | 00.151-113 | Paul Wild | 23.04. |
Tutorien
Eine Auflistung der Termine wird demnächst veröffentlicht.
Die Anmeldung zu den Tutorien erfolgt in der ersten Semesterwoche über StudOn. Beginn der Übungen und der Intensivübung ist in der zweiten Vorlesungswoche, also ab dem 20.04.
Die Abgabe der Übungen erfolgt wöchentlich in Gruppen von 3 Personen. Die Personen einer Abgabegruppe müssen dabei nicht in der gleichen Übungsgruppe angemeldet sein.
Wichtig: Die Abgabe erfolgt digital über StudOn. Eine Abgabe auf Papier ist nur noch direkt über Ihren Tutor möglich. Vermerken Sie bei Papierabgaben bitte auf der ersten Seite ihrer Abgaben stets die Namen und IdM-Kennungen aller Gruppenteilnehmer, damit wir die Abgaben richtig zuordnen können (ein entsprechendes Deckblatt für Papierabgaben ist im StudOn-Kurs verfügbar).
Übungsblätter
Die Blätter enthalten Präsenzaufgaben für die Tutorien und bepunktete Hausaufgaben, die über StudOn abgegeben werden können und für die Sie eine Korrektur erhalten. Die Übungsblätter werden auf StudOn veröffentlicht.
Inhalt
- Termersetzung
- Datentypen und Kodatentypen
- Reguläre Sprachen und endliche Automaten
- Induktion und Koinduktion
- λ-Kalkül
- Typsysteme
Skript
Es gibt ein auf einer studentischen Mitschrift vom SoSe 2014 basierendes Skript (Stand 09.07.2025), das im Laufe der Veranstaltung überarbeitet wird. 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.
Klausur
- Zur Klausur ist als Hilfsmittel ein beidseitig beschriebenes oder bedrucktes DIN-A4-Blatt zugelassen.
- Wir empfehlen einen rechtzeitigen Blick auf die Probeklausur, die wir gegen Ende der Vorlesungszeit veröffentlichen werden (hier gibt es die Probeklausur 2025). Beachten Sie, dass diese unverbindlichen Charakter hat; insbesondere garantieren wir nicht, dass alle Aufgabentypen aus der Probeklausur auch in der tatsächlichen Klausur vorkommen, und umgekehrt.
Literatur
Termersetzungssysteme
- 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
λ-Kalkül
- Ryo Kashima. A proof of the standardization theorem in λ-calculus
- Masako Takahashi. Parallel reductions in λ-calculus
- 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 λ-calculus
- M. Felleisen, Programming Languages and Lambda Calculi, 1998
Weitere
- 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