Übersicht
| Dozent: | Prof. Tobias Nipkow |
| Bereich: | Spezialvorlesung im Grundstudium: 2 Std. (+2 Ü) |
| Zeit und Ort: | Do. 8:30 - 10:00 Uhr, MI 00.08.059 |
| Beginn: | 5.5.2011 |
| TUM online |
Inhalt
In der Vorlesung werden ausgewählte Themen aus verschiedenen Bereichen der (hauptsächlich theoretischen) Informatik angesprochen:
- Primzahlzertifikate
- Lambda-Kalkül
- Logik
- Interaktives Beweisen mit Isabelle
- Funktionale Programmierung
- Endliche Automaten
- Entscheidungsverfahren für Arithmetik
Ziel der Vorlesung ist es, die Studierenden bereits zu Beginn ihres Studiums an Forschungsthemen heranzuführen.
Voraussetzungen: keine
Proseminar
Ein Teil der Vorlesung findet als Proseminar statt:
- Florian Gerlach: Pratts Primzahlzertifikate
- Manuel Eberl: Der untypisierte Lambda-Kalkül
- Steffen Smolka: Einfach getypter Lambda-Kalkül (Folien)
- Maximilian Moll: Aussagenlogik
Zur Vortragsvorbereitung: How To Present a Paper in Theoretical Computer Science: A Speaker's Guide For Students
Literatur
- Michael Huth and Mark Ryan. Logic in Computer Science. Cambridge University Press.
- John Hughes. Why Functional Programming Matters.
Übungen
| Übungsleitung: | Alexander Krauss |
| Zeit und Ort: | Fr. 10:00 - 11:30 Uhr, MI 01.09.014 ("Alonzo Church") |
| Beginn: | 6.5.2011 |
- 1. Übung: [Blatt 1] [pratt.tar.gz]
- 2. Übung: [Blatt 2]
- 3. Übung: [Blatt 3]
- 4. Übung: [Blatt 4]
- 5. Übung: [Blatt 5]
- 6. Übung: [Blatt 6] [Lösung]
- 7. Übung: [Blatt 7]
- 8. Übung: [Blatt 8]
- 9. Übung: [Blatt 9]
- 10.+11. Übung: [Stand vom 22.7.: Pratt.thy]
Isabelle
Sowohl in der Vorlesung als auch in den Übungen wird der interaktive Beweiser Isabelle eingesetzt. Dafür gibt es ein extra für die Perlen produziertes Installationspaket. Es gilt folgende Installationsanleitung wobei lediglich das Archiv durch ein anderes ausgetauscht ist.
Linux: Isabelle_09-Jun-2011_bundle_x86-linux.tar.gz.
Windows/Cygwin: Isabelle_09-Jun-2011_bundle_x86-cygwin.tar.gz.