[logic-ml] 【時間変更】JAIST Logic Seminar Series

[Hajime Ishihara]

皆様

以下のミュンヘン大学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: ishihara at jaist.ac.jp

(2014/02/08 16:07), Hajime Ishihara wrote:
> 皆様
>
> ミュンヘン大学のHelmut Schwichtenberg先生の連続講演のお知らせです。
> ふるってご参加ください。
>
> 問合せ先：
> 石原　哉
> 北陸先端科学技術大学院大学 情報科学研究科
> e-mail: ishihara at jaist.ac.jp
>
> --------------------------------------------------
> * 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.
>


-- 
Professor Hajime Ishihara
School of Information Science
Japan Advanced Institute of Science and Technology
1-1 Asahidai, Nomi, Ishikawa 923-1292, Japan
Tel: +81-761-51-1206
Fax: +81-761-51-1149
ishihara at jaist.ac.jp
http://www.jaist.ac.jp/~ishihara

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.fos.kuis.kyoto-u.ac.jp/pipermail/logic-ml/attachments/20140227/4ba88c6e/attachment.html>