皆様

ミュンヘン大学のHelmut Schwichtenberg先生の連続講演のお知らせです。
ふるってご参加ください。

問合せ先：
石原　哉
北陸先端科学技術大学院大学 情報科学研究科
e-mail: [email protected]

--------------------------------------------------
* JAIST Logic Seminar Series *

* This seminar is held as a part of the EU FP7 Marie Curie Actions
IRSES project CORCON.

Date: Wednesday 5, Thursday 6, Friday 7 March, 2014, 15:10-16:40

Place: JAIST, Lecture room I1
(Access: http://www.jaist.ac.jp/english/location/access.html)

Speaker: Professor Helmut Schwichtenberg
(Ludwig-Maximilians-Universitaet Muenchen, Germany)

Title: Computational content of proofs

*Wednesday 5 March, 2014, 15:10-16:40*

Lecture 1. Computing with partial continuous functionals.

We define computable functionals of finite type, with the Scott-Ersov
partial continuous functionals as domains. A term language T+ (a
common extension of Goedel's T and Plotkin's PCF) is introduced to
denote computable functionals.

*Thursday 6 March, 2014, 15:10-16:40*

Lecture 2. A theory of computable functionals.

Based on T+ we define a logical language whose quantifiers range over
partial continuous functionals and whose predicates are inductively
defined. We obtain a theory TCF of computable functionals by adding
introduction and elimination axioms for inductive predicates to
minimal logic. TCF admits a realizability interpretation (by terms in
T+) and a soundness theorem can be proved.

*Friday 7 March, 2014, 15:10-16:40*

Lecture 3. Extracting programs from proofs.

Every constructive proof of an existential theorem (or problem;
Kolmogorov 1932) contains a construction of a solution. To get hold
of such a solution we have two methods. (a) Write-and-verify. Guided
by the constructive proof directly write a program to compute the
solution, and then prove (verify) that this is the case. (b)
Prove-and-extract. Formalize the proof and extract its computational
content in the form of a realizing term t. Since the latter approach
requires formalization of the proof it is less popular. But it has
advantages. (i) Dealing with a problem on the proof level allows
abstract mathematical tools and a good organization of the material.
Both help to adapt the proof to changed specifications. (ii) The
extracted term can be automatically verified, by means of a
formalization of the soundness theorem. As an example of the
prove-and-extract method we build a parser for the Dyck language of
balanced parentheses.