皆様
ミュンヘン大学のHelmut Schwichtenberg先生の連続講演のお知らせです。
ふるってご参加ください。
問合せ先:
石原 哉
北陸先端科学技術大学院大学 情報科学研究科
e-mail: ishihara(a)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(a)jaist.ac.jp
http://www.jaist.ac.jp/~ishihara
皆様、
重複して受け取られた場合はどうぞご容赦ください。
北陸先端科学技術大学院大学の佐野勝彦です。
Computability Theory and Foundations ofMathematics 2014 の直後の 2/21, 2/22 に
金沢で開催する Epistemic Logic に関する国際ワークショップについて、
開催が迫りましたので、再度ご案内を致します。
===========================================
Kanazawa Workshop for Epistemic Logic and its Dynamic Extensions
-- JAIST Logic Workshop Series 2014 --
Dates: February 21-22, 2014
Venue: Shiinoki Cultural Complex, Kanazawa, Ishikawa, Japan
Website: http://www.jaist.ac.jp/~v-sano/jw2014/index.html
===========================================
Kanazawa Workshop for Epistemic Logic and its Dynamic Extensions will
be held at the Shiinoki Cultural Complex, and is organized by Satoshi
Tojo and Katsuhiko Sano of Japan Advanced Institute of Science and
Technology from 21st to 22nd February, 2014. The aim of the workshop
is to discuss about epistemic logic and dynamic epistemic logic and
their application from theoretical and practical viewpoints.
Invited Speakers:
Thomas Ågotnes (University of Bergen)
Mamoru Kaneko (Waseda University)
Hidenori Kurokawa (Kobe Univeristy)
Minghui Ma (Southwest University)
François Schwarzentruber (ENS Rennes)
Jeremy Seligman (The University of Auckland)
Sonja Smets (ILLC, Universiteit van Amsterdam)
Nobu-Yuki Suzuki (Shizuoka University)
Fernando R. Velázquez Quesada (Universidad de Sevilla)
Tomoyuki Yamada (Hokkaido University)
--
Katsuhiko Sano
School of Information Science
Japan Advanced Institute for Science and Technology
IS building No.1 7F, 1-1 Asahidai,
Nomi, Ishikawa, 923-1292, Japan
皆様、
千葉大学の新井敏康先生の講演のお知らせです。
どうぞふるってご参加ください。
問合せ先:
佐野 勝彦
北陸先端科学技術大学院大学 情報科学研究科
e-mail: v-sano(a)jaist.ac.jp
--------------------------------------------------
* JAIST Logic Seminar Series *
Date: Thursday 20th February 2014, 15:00-16:30
Place: Collaboration room 7 (I-56) (Access:
http://www.jaist.ac.jp/english/location/access.html)
Speaker: Prof. Toshiyasu ARAI (Chiba University)
Title: Proof search in intuitionistic logics
Abstract: Following G. Mints, we present a complete proof search in
multi-succedent sequent calculi for intuitionistic propositional and
pure predicate logic in the spirit of Schuette's schema.
皆様、
参加登録の締め切りが2月7日に迫って参りましたので、
再び案内をさせていただきます。
2月17日(月)~2月20日(木)に東京工業大学
Computability Theory and Foundations of Mathematics 2014
を開催致します。
研究集会のプログラムが
http://www.jaist.ac.jp/CTFM/CTFM2014/timetable.html
にてご覧いただけます。
宜しく参加をご検討ください。
横山
============================================================
Computability Theory and Foundations of Mathematics
(Tokyo Institute of Technology, Tokyo, Japan, February 17 - 20, 2014)
Conference webpage
http://www.jaist.ac.jp/CTFM/CTFM2014/index.html
Registration deadline: February 7.
Invited Speakers
Chong Chi Tat (National University of Singapore)
Damir Dzhafarov (University of Connecticut)
Cameron Freer (Massachusetts Institute of Technology and Analog
Devices Lyric Labs)
Hajime Ishihara (JAIST)
Akinori Kawachi (Tokyo Institute of Technology)
Akitoshi Kawamura (University of Tokyo)
Takayuki Kihara (JAIST)
Antonio Montalbán (University of California, Berkeley)
Ng Keng Meng (Nanyang Technological University)
Jan Reimann (Pennsylvania State University)
Paul Shafer (Ghent University)
Stephen G. Simpson (Pennsylvania State University)
Henry Towsner (University of Pennsylvania)
Wang Wei (Sun Yat-sen University)
Wu Guohua (Nanyang Technological University)
Organising Committee
Hajime Ishihara (JAIST)
Ryo Kashima (Tokyo Institute of Technology, local chair)
Sam Sanders (Ghent)
Stephen G. Simpson (Pennsylvania State University)
Kazuyuki Tanaka (Tohoku, chair)
Keita Yokoyama (JAIST)
Programme Committee
Kojiro Higuchi (Chiba)
Takayuki Kihara(JAIST)
Kenshi Miyabe(Tokyo)
Takako Nemoto(JAIST)
Sam Sanders (Ghent)
Takeshi Yamazaki (Tohoku)
Keita Yokoyama (JAIST, chair)
Keisuke Yoshii (Tohoku)
============================================================
どうぞよろしくお願い致します。
横山啓太
--
Keita Yokoyama
y-keita(a)jaist.ac.jp