Fakultät für Informatik

TU München - Fakultät für Informatik

TUM

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

 
 
Bereich: Spezialvorlesung im Grundstudium: 2 Std. (+2Ü)
Zeit und Ort: Do. 8:30 - 10:00 Uhr, MI 00.09.022
Beginn: 18.4.2007
Übungstermin: Do. 13:15 - 14:45, Raum: MI 00.09.55 (Alan Turing)
Übungsleitung: Alex Krauss
Mailingliste: Siehe https://mailmanbroy.in.tum.de/mailman/listinfo/perlen06

News

  • Einen Interpreter für den λ-Kalkül gibt es hier.
  • Ab dem 24.5. wird die Übung rechnergestützt stattfinden. Wer einen Laptop hat möge diesen bitte mitbringen, und vorher Isabelle installieren (s.u.)

Inhalt

In der Vorlesung werden ausgewählte Themen aus verschiedenen Bereichen der (hauptsächlich theoretischen) Informatik angesprochen:

  • Primzahltests
  • Unifikation
  • 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

Literatur

Übungsblätter

Isabelle

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

~isabelle/bin/Isabelle

Wer Isabelle auf dem eigenen Rechner installieren will, findet die nötigen Pakete samt Installationsanleitung unter http://isabelle.in.tum.de/dist-Isabelle_07-May-2007. Man braucht dafür Linux und einen installierten XEmacs.

Als Alternative gibt es unter obiger URL auch eine fertige Installation in einer virtuellen Maschine (ein komplettes Linux mit Isabelle und allen benötigten Komponenten), die sich dann auch unter Windows verwenden lässt.

Falls Schwierigkeiten bei der Installation auftreten, meldet euch bei mir (krauss(at)in.tum.de).

Unterlagen zu Isabelle

Alle Folien (zum Drucken)
Einführung Teil 1 Slides [pdf] Demo.thy
Einführung Teil 2 Slides [pdf] Demo.thy
Datentypen und Funktionen Slides [pdf] Demo.thy
Logik Slides [pdf] Demo1.thy Demo2.thy
Isar Slides [pdf] Demo1.thy Demo2.thy