Übersicht
| Dozent: | Prof. Tobias Nipkow |
| Bereich: | Spezialvorlesung im Grundstudium: 2 Std. (+2 Ü) |
| Zeit und Ort: | Do. 8:30 - 10:00 Uhr, MI 00.09.022 |
| Beginn: | 23.4.2009 |
| Mailingliste: | siehe https://mailmanbroy.in.tum.de/mailman/listinfo/perlen08 |
Inhalt
In der Vorlesung werden ausgewählte Themen aus verschiedenen Bereichen der (hauptsächlich theoretischen) Informatik angesprochen:
- Primzahltests
- Lambda-Kalkül
- Logik
- Interaktives Beweisen
- Funktionale Programmierung
- Endliche Automaten
- Entscheidungsverfahren für Arithmetik
Ziel der Vorlesung ist es, in enger Interaktion mit den teilnehmenden Studierenden bereits zu einem sehr frühen Stadium einen Bezug zu aktuellen Forschungsthemen herzustellen. Eine aktive und engagierte Mitarbeit ist unbedingte Teilnahmevoraussetzung.
Hörerkreis: Teilnehmer am Begabtenförderungsprogamm der Fakultät und andere Interessierte.
Voraussetzungen: keine
Unterlagen
Literatur
- Michael Huth and Mark Ryan. Logic in Computer Science. Cambridge University Press.
- John Hughes. Why Functional Programming Matters.
Übungen
| Übungsleitung: | Florian Haftmann |
| Zeit und Ort: | Do. 10:15 - 11:45 Uhr, MI 00.11.038 (»John von Neumann«, 11er-Flügel Erdgeschoß) |
| Beginn: | 30.4.2009 |
Übungsblätter
- 1. Übungsblatt (PDF)
- 2. Übungsblatt (PDF)
- 3. Übungsblatt (PDF)
- 4. Übungsblatt (PDF)
- 5. Übungsblatt (PDF)
- 6. Übungsblatt (PDF)
- 7. Übungsblatt (PDF) mit Rahmentheorie
Isabelle
Für einige Übungen werden wir den interaktiven Beweiser Isabelle einsetzen.
Installation
Isabelle läuft unter gängigen UNIX-artigen Systemen, siehe Installationsanleitung.
Windows-Benutzer können Isabelle zusammen mit Cygwin verwenden. Details dazu ebenfalls in der Installationsanleitung.
Falls Schwierigkeiten bei der Installation auftreten, einfach eine kurze E-Mail an mich senden.
Unterlagen zu Isabelle
Alle Folien (zum Drucken)| Einführung | Demo.thy Demo.thy |
| Datentypen und Funktionen | Demo.thy |
| Simplifikation | Demo.thy |
| Induktionsheuristiken | Demo.thy |
| Logik | Demo1.thy Demo2.thy |
| Isar | Demo1.thy Demo2.thy DemoAVL.thy |