Department Mathematik
print


Navigationspfad


Inhaltsbereich

Seminar: Programmextraktion aus Beweisen

Zeit und Ort

Mo 14-16, B252; Beginn 15. April 2013. Am 29. April fällt das Seminar aus.

Inhalt

Es sollen Theorie und Praxis der Extraktion von Programmen aus Beweisen erarbeitet werden. Vorausgesetzt werden Kenntnisse in Mathematischer Logik (eine einführende Vorlesung, insbesondere Vertrautheit mit Gentzens System des natürlichen Schließens). Ferner wird vorausgesetzt, daß die Teilnehmer das Tutorium des Beweisassistenten Minlog durchgearbeitet haben.

Vorträge

  • Einführung in die konstruktive Analysis. Helmut Schwichtenberg, 22. April
  • Rechnerischer Gehalt von Beweisen in der konstruktiven Analysis, Helmut Schwichtenberg, 6. Mai
  • Der Satz vom abgeschlossenen Graphen (Ishihara). Katrin Gold, 13. und 27. Mai
  • Realisierbarkeit und induktive Definitionen (Tatsuta):Korrektheitssatz, Beispiele. David Korinth, 3. und 10. Juni
  • Eine formale Theorie der Berechenbarkeit in höheren Typen. Christian Saile, 17. Juni und 1. Juli
  • Realisierbarkeit für abstrakte Theorien. Christine Birkmüller, 8. Juli
  • Programmextraktion mit reellen Zahlen als Strömen. Verena Reinl, 15. Juli

Materialien

Tutorium

Es wird ein Tutorium angeboten. Tutor: Kenji Miyamoto. Mo 10-12, Ort noch offen (vorläufig B420)

Sprechstunden

Letzte Änderung

24. April 2013