In my Department there will be a very interesting PhD-level course, organized by my colleague and friend Marco Benini. I quote from his presentation:
Computational content of proofsWe consider logical propositions concerning data structures. If such a proposition involves (constructive) existential quantifiers in strictly positive positions, then -- according to Brouwer, Heyting and Kolmogorov -- it can be seen as a computational problem. A (constructive) proof of the proposition then provides a solution to this problem, and one can machine extract (via a realizability interpretation) this solution in the form of a lambda calculus term involving recursion operators, which can be seen as (and translated into) a functional program. We will develop from scratch the theory of (1) computability in higher types, based on Scott's information systems, and (2) realizability interpretations of a logic of inductive definitions. A special emphasis will be on the question how to control at the proof level the complexity of the extracted programs.
This PhD-level course is kindly held by Professor H. Schwichtenberg, Mathematisches Institut, Fakultät für Mathematik, Informatik und Statistik, Ludwig Maximillians Universität - Muenchen (DE). This PhD-level course is held under the Erasmus program. There is no final examination. If a student needs an attendance certification, please, contact Prof. Marco Benini by email.
Schedule
In Sala riunioni, third floor of Dipartimento di Informatica e Comunicazione, via Mazzini 5, 21100 Varese (VA).
Dates: 2nd, 3rd, 6th and 7th October 2008, 11:00 to 12:30 and 14:30 to 16:00.
No comments:
Post a Comment