Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Mini-VL “Konstruktive Logik und Progrmmextraktion”
Im Rahmen des Visiting Professorship Programme der FAU wird Dr. Dirk Pattinson von der Australian National University in Canberra ein Mini-Vorlesung zum Thema “Constructive Logic and Program Extraction” abhalten. Die beiden Termine sind
- und 26.09.2013, jeweils von 14.00 - 16.00 Uhr
Raum 11.150, blaues Hochhaus (Seminarraum INF8).
Kurzbeschreibung:
The ability to extract programs from proofs is one of the most distinctive features of constructive logic.
We explore the foundations of constructive logic and make the notion of ‘computational content’ of
constructive proofs precise. Extracted programs can embody this computational content, and provably
satisfy their specifications.
Lecture 1: – Introduction to constructive logic and reasoning, examples
– From proofs to Turing machines: Kleene’s number realisability
Lecture 2: – Goedel’s system T
– From proofs to functional programs: Kreisel’s modified realisability
Time permitting we will also discuss categorical models (modest sets) and show how realisability
can be used as a tool to establish independence results.
Die Veranstaltung ist für Studierende gedacht; ich möchte insofern zur zahlreichen Teilnahme ermutigen.
– Lutz Schröder
Wird es Aufzeichnungen der Vortraege/Mini-VL geben?
1 „Gefällt mir“