<html>
<head>
<meta content="text/html; charset=ISO-2022-JP"
http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">$B3'MM(B<br>
<br>
$B0J2<$N%_%e%s%X%sBg3X(BHelmut Schwichtenberg$B@h@8$NO"B39V1i$NFb(B<br>
3$B7n(B6$BF|!JLZ!K$N;~4V$,JQ99$K$J$j$^$7$?!#(B<br>
$B>l=j$OJQ99$4$6$$$^$;$s!#(B<br>
$B$U$k$C$F$4;22C$/$@$5$$!#(B<br>
<br>
*Thursday 6 March, 2014, <b>13:30-15:00</b>*<br>
<br>
Lecture 2. A theory of computable functionals.<br>
<br>
Based on T+ we define a logical language whose quantifiers range
over<br>
partial continuous functionals and whose predicates are
inductively<br>
defined. We obtain a theory TCF of computable functionals by
adding<br>
introduction and elimination axioms for inductive predicates to<br>
minimal logic. TCF admits a realizability interpretation (by terms
in<br>
T+) and a soundness theorem can be proved.<br>
<br>
$BLd9g$;@h!'(B<br>
$B@P86!!:H(B<br>
$BKLN&@hC<2J3X5;=QBg3X1!Bg3X(B $B>pJs2J3X8&5f2J(B<br>
e-mail: <a class="moz-txt-link-abbreviated" href="mailto:ishihara@jaist.ac.jp">ishihara@jaist.ac.jp</a><br>
<br>
(2014/02/08 16:07), Hajime Ishihara wrote:<br>
</div>
<blockquote cite="mid:52F5D7C8.60304@jaist.ac.jp" type="cite">
<pre wrap="">$B3'MM(B
$B%_%e%s%X%sBg3X$N(BHelmut Schwichtenberg$B@h@8$NO"B39V1i$N$*CN$i$;$G$9!#(B
$B$U$k$C$F$4;22C$/$@$5$$!#(B
$BLd9g$;@h!'(B
$B@P86!!:H(B
$BKLN&@hC<2J3X5;=QBg3X1!Bg3X(B $B>pJs2J3X8&5f2J(B
e-mail: <a class="moz-txt-link-abbreviated" href="mailto:ishihara@jaist.ac.jp">ishihara@jaist.ac.jp</a>
--------------------------------------------------
* 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: <a class="moz-txt-link-freetext" href="http://www.jaist.ac.jp/english/location/access.html">http://www.jaist.ac.jp/english/location/access.html</a>)
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.
</pre>
</blockquote>
<br>
<br>
<pre class="moz-signature" cols="72">--
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
<a class="moz-txt-link-abbreviated" href="mailto:ishihara@jaist.ac.jp">ishihara@jaist.ac.jp</a>
<a class="moz-txt-link-freetext" href="http://www.jaist.ac.jp/~ishihara">http://www.jaist.ac.jp/~ishihara</a>
</pre>
</body>
</html>