皆様
ミュンヘン大学の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.
皆様
以下のミュンヘン大学Helmut Schwichtenberg先生の連続講演の内 3月6日（木）の時間が変更になりました。 場所は変更ございません。 ふるってご参加ください。
*Thursday 6 March, 2014, *13:30-15:00**
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.
問合せ先： 石原 哉 北陸先端科学技術大学院大学 情報科学研究科 e-mail: [email protected]
(2014/02/08 16:07), Hajime Ishihara wrote:
皆様
ミュンヘン大学の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.
-
Hajime Ishihara