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