TU München - Fakultät für Informatik
Software- and Systems Engineering Research Group

  Home  |  Forschung/Kompetenz  |  Lehre  |  Personen  |  Publikationen  |  Abschlussarbeiten  |  Sonstiges  |  Kontakt  | 

Vorlesung | Sommersemester 2008
Perlen der Informatik 2
Prof. Tobias Nipkow

News

• Einen Interpreter für den λ-Kalkül gibt es hier.

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

• Pratts Primzahlzertifikate
• Miller-Rabin
• Aussagenlogik
• Untypisierter Lambda-Kalkül
• Presburger Arithmetik
• Haskell
• Huffman

Literatur

• Michael Huth and Mark Ryan. Logic in Computer Science. Cambridge University Press.
• John Hughes. Why Functional Programming Matters.

Übungsblätter

• 1. Übungsblatt (PDF)
• 2. Übungsblatt (PDF)
• 3. Übungsblatt (PDF)
• 4. Übungsblatt (PDF)
• 5. Übungsblatt (PDF)
• 6. Übungsblatt (PDF)
• 7. Übungsblatt (PDF)
• 8. Übungsblatt (PDF) mit Rahmentheorie

In den letzten Übungen am 4., 11. & 18. Juli wird es keine Übungsblätter geben; statt dessen besteht für alle Interessierten die Möglichkeit, »freischaffend« mit dem Isabelle-System zu experimentieren und dabei aufkommende Fragen zu stellen.

Isabelle

Für einige Übungen werden wir den interaktiven Beweiser Isabelle einsetzen. Isabelle ist auf der Rechnerhalle installiert und kann dort wie folgt lokal gestartet werden:

Ein Arbeiten remote ist wegen subtiler X-Probleme nicht zwingend möglich.

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, meldet euch bei mir.

Unterlagen zu Isabelle