- Kisoron-ml - fos.kuis.kyoto-u.ac.jp

Ninth NII Type Theory Workshop
by Makoto Tatsuta 11 Jan '15

11 Jan '15

Ninth NII Type Theory Workshop Date: January 15, 2015, 10:20--17:30 Place: National Institute of Informatics, Room 1208 (12th floor) 場所: 国立情報学研究所 12階 1208室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Program: 10:20--11:00 Daisuke Kimura (National Institute of Informatics) Title: A framework of models of functional PTSs 11:00--11:40 Josh Ko (National Institute of Informatics) Title: Relational algebraic ornamentation 11:40--13:10 Lunch Break 13:10--13:50 Makoto Fujiwara (Tohoku University) Title: On the strength of ¥Delta^0_1-LEM over Intuitionistic Analysis 13:50--14:30 Koji Nakazawa (Kyoto University) Title: Confluence of lambda-calculi with permutative conversion 14:30--14:50 Break 14:50--15:30 Mahmudul Faisal Al Ameen (The Graduate University for Advanced Studies) Title: Completeness of Separation Logic with Recursive Procedures 15:30--16:10 Makoto Tatsuta (National Institute of Informatics) Title: Decidability of Separation Logic with Monadic Inductive Definitions 16:10--16:30 Break 16:30--17:30 Stefano Berardi (Torino University) Title: Realizability and Strong Normalization for Heyting Arithmetic with EM1 Abstracts: ---------------------------------------------------------------------- Daisuke Kimura (National Institute of Informatics) Title: A framework of models of functional PTSs Abstract: This talk presents a framework of models of functional PTSs. The class of functional PTSs is a class of PTS which contains well-known type theories such as the simply typed lambda calculus, System F, lambda P (dependent type system), and Calculus of Constructions. This framework of models is obtained by using Cousineau and Dowek's embedding from a functional PTS into a lambda P modulo. As a result of this talk, a semantical condition for a functional PTS to be a strongly normalizing system is given. This result is expected to give a semantical approach to Barendregt-Geuvers-Klop conjecture. ---------------------------------------------------------------------- Josh Ko (National Institute of Informatics) Title: Relational algebraic ornamentation Abstract: Type theory makes it possible to treat programs and proofs uniformly as the same entities. Dependently typed programmers aim to design programs that carry their own correctness proofs, exploiting the coincidence of programs and proofs to the full extent. A generic construction that can help to achieve this is relational algebraic ornamentation, with which we can synthesise datatypes satisfying properties that can be expressed in terms of folds. In this talk I will show how relational algebraic ornamentation can help with designing a dependently typed program for solving the well-known minimum coin change problem. ---------------------------------------------------------------------- Makoto Fujiwara (Tohoku University) Title: On the strength of ¥Delta^0_1-LEM over Intuitionistic Analysis Abstract: Ishihara [2] showed over intuitionistic analysis EL that Markov’s principle MP is equivalent to WMP+¥Pi^0_1-DML(under the name of MP^v). On the other hand, Akama et al. [1] showed that ¥Delta^0_1-LEM is implied from both of MP(under the name of ¥Sigma^0_1-DNE) and ¥Sigma^0_1-DML(under the name of ¥Sigma^0_1-LLPO). In this talk, we show over EL that ¥Delta^0_1-LEM is implied from ¥Pi^0_1-DML and equivalent to ¥Delta^0_1 comprehension axiom, which is from reverse mathematics. In addition, some separation results are also presented. This is a joint work with Hajime Ishihara and Takako Nemoto. References: [1] Y. Akama, S. Berardi, S. Hayashi and U. Kohlenbach, An arithmetical hierarchy of the law of excluded middle and related principles. Proc. of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), pp. 192--201, IEEE Press (2004). [2] H. Ishihara, Markov's principle, Church's thesis and Lindel¥"of theorem, Indag. Math. (N.S.) 4 (1993), pp. 321--325. ---------------------------------------------------------------------- Koji Nakazawa (Kyoto University) Title: Confluence of lambda-calculi with permutative conversion Abstract: We give a new proof of confluence for the lambda and the lambda-mu calculi with permutative conversion for case branching. For such calculi, naive approaches with parallel reductions do not work, and we adopt a proof technique with generalized notions of complete development with the Z property, introduced by Dehornoy and van Oostrom. Our idea also gives a simpler proof for confluence of the first-order classical natural deduction, which has been proved by Ando with more complicated notions. ---------------------------------------------------------------------- Mahmudul Faisal Al Ameen (The Graduate University for Advanced Studies) Title: Completeness of Separation Logic with Recursive Procedures Abstract: This talk proves the completeness of Hoare's Logic extended by separation logic for verification of while programs with pointers and recursive procedures. ---------------------------------------------------------------------- Makoto Tatsuta (National Institute of Informatics) Title: Decidability of Separation Logic with Monadic Inductive Definitions Abstract: This talk shows the decidability of entailments of symbolic heaps in separation logic with monadic inductive definitions under certain conditions. ---------------------------------------------------------------------- Stefano Berardi (Torino University) Title: Realizability and Strong Normalization for Heyting Arithmetic with EM1 Abstract: We present a new Curry-Howard correspondence for HA+EM1, first order constructive Heyting Arithmetic with the excluded middle on Sigma-0-1-formulas. We add to the lambda calculus an operator k_a which represents, from the viewpoint of programming, an exception operator with a delimited scope, and from the viewpoint of logic, a restricted version of the excluded middle. We motivate the restriction of the excluded middle by its use in proof mining; we introduce new techniques to prove strong normalization for HA + EM1 and the witness property for simply existential statements. One may consider our results as an application of the ideas of Interactive realizability, which we have adapted to the new setting and used to prove our main theorems. This technique has been recently extended by F. Aschieri to the entire excluded middle for First Order Arithmetic. This is a joint work with F. Aschieri and G. Birolo. ---------------------------------------------------------------------- 問合せ先　龍田 (tatsuta(a)nii.ac.jp)

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 10 Jan '15

10 Jan '15

皆様スワンジー大学のAnton Setzer先生の講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学研究科 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 projects COMPUTAL (http://computal.uni-trier.de/) and CORCON (http://corcon.net/). Date: Thursday 22 January, 2015, 15:10-16:40 Place: JAIST, Collaboration room 6 (I-57g) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Anton Setzer (Swansea University) Title: Extraction of programs from proofs using postulated axioms (joint work with Chi Ming Chuang) Abstract: In this talk we discuss how to extract programs from proofs with postulated axioms in dependent type theory. Since type theory has constructive logic, it is easy to determine for every $\Pi_2$-statement a function $f$ which determines the witness from the input. However, in the presence of postulated axioms, this function applied to an argument doesn't reduce necessarily to constructor head normal form, which means it doesn't produce a value. In this talk we discuss conditions which guarantee that the extracted function provide values in the presence of postulated axioms, and give a proof. This methodology will be applied to the extraction of alogrithms for exact real number computations. For this purpose the signed digit reals are introduced as a coalgebraic data type, and it is shown that the signed digit reals are closed under average, multiplication and rational numbers. Proofs have been carried out in the theorem prover Agda and the resulting programs can be executed effectively in this language.

1 0

東大数理集中講義のお知らせ
by 渡辺純成 09 Dec '14

09 Dec '14

基礎論歴史分科会MLの皆様、東京学芸大の渡辺純成です。数学史を主題とする集中講義（東京大数理科学研究科）のお知らせです。入試で忙しい時期になりますが、皆様、お誘い合わせの上、お出で下さい。なお、広くお知らせするために複数のメーリングリストに投稿しておりますが、重複して受け取られた方々にはご海容いただけますと幸いです。 ────2014年11月13日　渡辺純成 ============= 講師：中根美知代氏（日本大学理工学研究所）期日：2015 年 1 月 5 日（月）から 9 日（金）まで時間：１４時５０分から１６時５０分まで場所：東京大学大学院数理科学研究科（駒場）１２３講義室題名：解析学への歴史の試み：「代数解析」の新系譜概要：「解析」という語は、古代ギリシアから導入されているが、時代とともに、その意味が異なっている。「代数解析」で示される事柄も、近代・18世紀・19 世紀・現代では大きく変化している。この言葉を手がかりに、今日、「解析学」と呼ばれている分野が形成されていく過程を部分的に明らかにする。古代から18世紀までの「解析」の変化を概観して歴史の流れを掴んだ上で、19世紀の数学者たちの原論文を参照しながら、実際に理論が作られていく過程を見ていく。自分で数学史に取り組んでみようとするときに有用な、基礎的な知識もあわせて紹介していきたい。以下のような順序ですすめていく。 1．代数解析前史　古代ギリシアの解析・イスラームの「代数＝解析」との捉え方 2. 代数解析から無限小解析へ　Viète・Descartesによる代数＝解析の捉え方　17-18世紀における無限小解析の形成 3．教科としての「代数解析」　Euler の『無限解析序説』・Lagrange が名づけた「代数解析」　Cauchyが「代数解析」で講義したもの 4. 今日の微積分学の起源　Cauchyの教科書の成果と限界 Cauchyの不備はどのように乗り越えられたかエピローグ：Euler　と「今日の代数解析」

2 2

The 49th MLG Meeting: Program
by Katsuhiko Sano 01 Dec '14

01 Dec '14

$BBh(B49$B2s(B MLG $B?tM}O@M}3X8&5f=82q$N$40FFb(B $B!J=EJ#$7$F$*<u$1<h$j$N:]$O$4MF<O$/$@$5$$!#!K(B $BKLN&@hC<2J3X5;=QBg3X1!Bg3X$N:4Ln>!I'$G$9!#(B 2014$BG/EY(BMLG$B?tM}O@M}3X8&5f=82q!JBh(B49$B2s!K$r2<5-$NMWNN$G3+:E$7$^$9!#(B $B9V1i!&=IGq$N?=$79~$_$ODy$a@Z$j$^$7$?$,!$;22C$9$k$3$H$O2DG=$G$9!#(B $B$=$N>l9g!";22C?M?t$N4X78$G!$G0$N$?$a;d$^$G%a!<%k$G$40lJs$/$@$5$$(B $B!J;22CHq!J2q>lBe!K(B3000$B1_$r$$$?$@$/M=Dj$G$*$j$^$9!K!#(B $B$I$&$>$h$m$7$/$*4j$$$$$?$7$^$9!#(B ========================================= $BBh(B49$B2s(B MLG $B?tM}O@M}3X8&5f=82q3+:EMWNN(B ========================================= $B4|4V(B: 2014 $BG/(B 12 $B7n(B 5 $BF|(B($B6b(B) $B!A(B 12 $B7n(B 7 $BF|(B($BF|(B) $B>l=j(B: $B;3Cf29@t2O</Aq%m%$%d%k%[%F%k!J(BJR$B2C2l29@t1X$+$i<V$GLs(B20$BJ,!$2C2l29@t1X$+$iAw7^$"$j!K(B $B")(B922-0126 $B@P@n8)2C2l;T;3Cf29@t2O</D.%[(B100, URL : http://www.daiwaresort.jp/kajikasou/ $B%[!<%`%Z!<%8!'(Bhttps://sites.google.com/site/mlg2014kaga/ $B9V1i%W%m%0%i%`!'(B 12/5 (Fri) 1315--1325 $B3+2q(B (opening) 1325--1400 $B;3yu(B $B<S5*;R(B ($B<sETBg3XEl5~(B), Constructive Embedding from Logics of Strict Implication to Modal Logics via Cut-free and complete Labelled Sequent Calculus 1400--1435 $B6b;R(B $B<i(B ($BAa0pEDBg3X(B), Game Theoretic Decidability and Undecidability 1435--1510 $B4X(B $BN49((B ($B?73cBg3X(B), A Note on American Plan Semantics of Relevant Modal Logics 1530--1605 $B0KF#(B $B@.9'(B (JAIST), A relationship between classical and intuitionistic linear logic 1605--1640 $B>>ED(B $BD>M4(B ($BEl5~9)6HBg3X(B), Intuitionistic tree sequent calculus and intuitionistic lambda rho calculus 1640--1715 $BNkLZ(B $B?.9T(B ($B@E2,Bg3X(B), Two weak variants of existence property in intermediate predicate logics 12/6 (Sat) 0930--1005 $B2#9B(B $B63J?(B ($BF|K\Bg3X(B), $BCf4VO@M}$NItJ,BN7O$H$=$NJ]B83HBg$K$D$$$F(B 1005--1040 PREINING Norbert (JAIST), Separating intermediate predicate logics of well-founded and dually well-founded structures by monadic sentences 1100--1135 $B6bBt(B $B@?(B ($B9qN)>pJs3X8&5f=j(B), Toward a Logic of Cumulative Quantification 1135--1210 $B2#;3(B $B7<B@(B (JAIST), What is needed to characterize the natural number system? 1340--1415 $BEDCf(B $B5A?M(B ($B6e=#;:6HBg3X(B), Algebraic models for description logics 1415--1450 Jonni Virtema (JAIST), Tableau calculi for propositional dependence logics 1450--1510 $B:4!9LZ(B $B9nL&(B ($BFn;3Bg3X(B), The exact K4-models constructed from the exact S4-models 1530--1605 $BLnB<(B $B>0?7(B (JAIST), Revising a Labelled Sequent Calculus for Public Announcement Logic 1605--1640 $B5HB<(B $BOB?M(B (JAIST), A general analysis on proof structures 1900-- $B:)?F2q(B (Conference dinner) 12/7 (Sun) 0930--1005 $B2-:d(B $B>MJ?(B ($BElKLBg3X(B), Lindstrom extension on finite models 1005--1040 $B2CF#(B $BH%(B ($BEl5~9)6HBg3X(B), $BM-8B%U%l!<%`$K$*$1$kMMAjO@M}<0$N(Bvalidity$B$H7W;;NL$K$D$$$F(B 1100--1135 $BsnF#(B $B?.?C(B ($BEl5~9)6HBg3X(B), lambda-mu-calculus $B$N?d0\N'$N=|5n(B 1135--1210 $B:4F#(B $B2mI'(B ($B5~ETBg3XL>M@65<x(B), A name-free lambda-calculus 1210--1220 Closing --- MLG49 $B@$OC?M(B $B:4Ln>!I'!JKLN&@hC<2J3X5;=QBg3X1!Bg3X!K(B E-mail : mlg.logic.japan(a)gmail.com / katsuhiko.sano(a)gmail.com

1 0

再送：数学基礎論若手の会2014
by YOSHIDA Satoru 04 Nov '14

04 Nov '14

皆様重複して受け取られた場合はご容赦ください。数学基礎論若手の会2014について、参加申込み締切を下記の通り延長致しました：講演、参加、宿泊の申込み： 2014年11月18日15時（開催日前日）. 宿泊施設での食事の申込み：2014年11月13日15時. まだ多少時間がありますので、講演をご検討頂けたらと思います。また、講演プログラム（暫定版）および参加者リストを後述の若手の会webサイト内に掲載しました。以上、よろしくお願い致します。 2014年9月22日 19:04 YOSHIDA Satoru <satoru-y(a)kankyo-u.ac.jp>: > 皆様 > > 重複して受け取られた場合はご容赦ください。 > > 数学基礎論若手の会2014のご案内です。 > > 数学基礎論を専攻する学生および若手研究者の研究交流を目的とす > る合宿形式の研究集会です． > 講演はオリジナルの成果発表に限らず，研究の途中報告や研究内容の紹介など幅広く募集しております． > また，これから数学基礎論を勉強したいと思っている方のご参加も歓迎します． > 多くの方々のご参加およびご講演をお待ちしています． > > 日程：11月19日（水）午後－21日（金）午前 > 場所：鳥取市サイクリングターミナル砂丘の家（鳥取砂丘付近） > http://www.city.tottori.lg.jp/www/contents/1198114185831/ > 幹事：吉田聡（鳥取環境大学） satoru-y(a)kankyo-u.ac.jp > ホームページ： http://misc.kankyo-u.ac.jp/~satoru-y/wakate14/ > > 今年度若手の会申込み要領については上記ホームページをご参照ください。 > > > -- > 吉田聡<YOSHIDA, Satoru> > 鳥取環境大学 > -- 吉田聡<YOSHIDA, Satoru> 鳥取環境大学

1 0

第49回 MLG 数理論理学研究集会のご案内（再送：講演・宿泊の申し込み締め切り11/21）
by Katsuhiko Sano 30 Oct '14

30 Oct '14

第49回 MLG 数理論理学研究集会のご案内 (重複してお受け取りの際はどうぞご容赦ください。) 北陸先端科学技術大学院大学の佐野勝彦と申します。締め切りまで三週間程となりましたので、再度アナウンスさせていただきます。 2014年度MLG数理論理学研究集会（第49回）を下記の要領で開催いたします。多くの方のご講演・ご参加をお待ちしております。 ========================================= 第49回 MLG 数理論理学研究集会開催要領 ========================================= - 期間: 2014 年 12 月 5 日(金) 〜 12 月 7 日(日) - 場所: 山中温泉河鹿荘ロイヤルホテル（JR加賀温泉駅から車で約20分，加賀温泉駅から送迎あり） -- 〒922-0126 石川県加賀市山中温泉河鹿町ホ100 -- URL : http://www.daiwaresort.jp/kajikasou/ - 講演・宿泊申込締め切り: 2014 年 11 月 21 日（木） - 申し込みはこちらから --> http://goo.gl/RfZ5SE - ホームページ: https://sites.google.com/site/mlg2014kaga/ - 連絡先E-mail: mlg.logic.japan [at] gmail.com ============ 参加募集 ============ - 講演時間は原則40分を予定しています。 - 12月6日（土）の夜に懇親会を行います。 - 全日程参加の場合，参加費（宿泊代・食事代・会場代）は25000円前後になる予定です。 - ご講演をなさらなくても参加いただけます。山中温泉河鹿荘ロイヤルホテルで宿泊および食事をなさらない場合にも参加費（会場代）3000円をいただきます。 - 参加・講演申し込みは、http://goo.gl/RfZ5SE の registration form からお願い致します。世話人: 佐野勝彦〒923-1292 石川県能美市旭台1-1 北陸先端科学技術大学院大学情報科学研究科 MLG2014 に関するメールは，mlg.logic.japan [at] gmail.com まで。

1 0

再送：数学基礎論若の手会（10/29締切）
by YOSHIDA Satoru 17 Oct '14

17 Oct '14

皆様重複して受け取られた場合はご容赦ください。数学基礎論若手の会2014のご案内です。数学基礎論を専攻する学生および若手研究者の研究交流を目的とする合宿形式の研究集会です．講演はオリジナルの成果発表に限らず，研究の途中報告や研究内容の紹介など幅広く募集しております．また，これから数学基礎論を勉強したいと思っている方のご参加も歓迎します．多くの方々のご参加およびご講演をお待ちしています．日程：11月19日（水）午後－21日（金）午前場所：鳥取市サイクリングターミナル砂丘の家（鳥取砂丘付近） http://www.city.tottori.lg.jp/www/contents/1198114185831/ 幹事：吉田聡（鳥取環境大学） satoru-y(a)kankyo-u.ac.jp ホームページ： http://misc.kankyo-u.ac.jp/~satoru-y/wakate14/ 申込み要領については上記ホームページをご参照ください。 -- 吉田聡<YOSHIDA, Satoru> 鳥取環境大学

1 0

PSSJ Symposium
by takeuti＠kuis.kyoto-u.ac.jp 16 Oct '14

16 Oct '14

各位科学哲学会シンポジウムの宣伝を致します。シンポジウム「数学を巡る思索」日時：11月15日（土）14:15〜16:45 会場：南山大学名古屋キャンパスＢ棟B11教室ウェブ：http://pssj.info/program/program.html 会費が1000円掛かります。数学史の観点からは、野本和幸氏のデデキントの数概念に関する講演があります。数学としての話はありません。産総研竹内泉 takeuti(a)ni.aist.go.jp

1 0

JAIST Logic Seminar Series (18th Sep. 2014: Tadeusz Litak on Relational lattices)
by Katsuhiko Sano 22 Sep '14

22 Sep '14

皆様、 FAU Erlangen-Nürnberg の Tadeusz Litak さんの講演のお知らせです。ふるってご参加ください。問い合わせ先：佐野勝彦北陸先端科学技術大学院大学情報科学研究科 e-mail: v-sano(a)jaist.ac.jp ---------------------------------------------------------------------------------------------------- * JAIST Logic Seminar Series * Date: Thursday, 18th September, 2014, 15:10-17:00 Place: JAIST Collaboration Room 6 (I57-g) (Access:http://www.jaist.ac.jp/english/location/access.html) Speaker: Tadeusz Litak (Department Informatik, Technische Fakultät, FAU Erlangen-Nürnberg, Germany) Title: Relational lattices Abstract: We study an interpretation of lattice connectives as natural join and inner union between database relations with non-uniform headers. We show that this interpretation proposed by database experts (Vadim Tropashko from Oracle) yields a class of lattices which has not been considered in the existing lattice-theoretical literature. We discuss axiomatizability and decidability of their (quasi-)equational theory and propose an equational axiomatization for a corresponding abstract algebraic class. It turns out that addition of just the “header constant” to the lattice signature already allows mimicking the Maddux technique for cylindric algebras and encode the word problem for semigroups in the quasiequational theory. Relational lattices, however, are not as intangible as one may fear: for example, they do form a pseudoelementary class. We also apply the tools of Formal Concept Analysis and investigate standard contexts of relational lattices, obtaining, e.g., results on their subdirect irreducibility. This is a joint work with Szabolcs Mikulas and Jan Hidders ----------------------------------------------------------------------------------------------------

2 2

再送：数学基礎論若手の会
by YOSHIDA Satoru 22 Sep '14

22 Sep '14

皆様重複して受け取られた場合はご容赦ください。数学基礎論若手の会2014のご案内です。数学基礎論を専攻する学生および若手研究者の研究交流を目的とする合宿形式の研究集会です．講演はオリジナルの成果発表に限らず，研究の途中報告や研究内容の紹介など幅広く募集しております．また，これから数学基礎論を勉強したいと思っている方のご参加も歓迎します．多くの方々のご参加およびご講演をお待ちしています．日程：11月19日（水）午後－21日（金）午前場所：鳥取市サイクリングターミナル砂丘の家（鳥取砂丘付近） http://www.city.tottori.lg.jp/www/contents/1198114185831/ 幹事：吉田聡（鳥取環境大学） satoru-y(a)kankyo-u.ac.jp ホームページ： http://misc.kankyo-u.ac.jp/~satoru-y/wakate14/ 今年度若手の会申込み要領については上記ホームページをご参照ください。 -- 吉田聡<YOSHIDA, Satoru> 鳥取環境大学

1 0

Prof. Aleksy Schubert at NII Logic Seminar
by Makoto Tatsuta 22 Sep '14

22 Sep '14

Prof. Aleksy Schubert at NII Logic Seminar Date: September 26, 2014, 14:00--16:00 Place: National Institute of Informatics, Room 1716 (17th floor) 場所: 国立情報学研究所 17階 1716室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Prof. Aleksy Schubert (University of Warsaw) (1) Title: Undecidability and complexity in fragments of first-order intuitionistic logic Abstract: In case of classical first-order logic there is a full characterisation of decidable and undecidable classes of formulae depending on the quantifier prefix and the vocabulary that is used. First-order logic in intuitionistic case lacks this kind of classification since there is no prefix normal form and actually the prenex fragment of the logic is in many cases much weaker than the general calculus. However, there is one meaningful stratification of the intuitionistic logic similar to the prenex form. We can consider classes of formulae that would result in a particular prefix of quantifiers when transformed using classical equivalences. The status of decidable and undecidable cases within this stratification will be presented as well as the complexity of known subcases. (2) Title: Verification of programs using Frama-C and Why3 Abstract: Frama-C is a tool that makes it possible to do a variety of analyses for C programs annotated with C specification language called ACSL (The ANSI/ISO C Specification Langage). One of the possible ways to use Frama-C is to generate verification conditions for appropriately defined Hoare logic that is in line with C programming language semantics. These verification conditions can subsequently be discharged by Why3 tool that makes it possible to manage the proving of necessary properties. During the talk I will present an overview of the tools and show a number of interesting examples to demonstrate how these tools work together to make possible verification of practical programs. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

研究集会「高信頼な理論と実装のための定理証明および定理証明器」案内
by Yoshihito Tanaka 22 Sep '14

22 Sep '14

九州大学マス・フォア・インダストリ研究所の溝口先生の代理で投稿いたします． ========================================================================= 研究集会「高信頼な理論と実装のための定理証明および定理証明器」案内　　　　　　　　　　　　　　　　　　　(English version is below.) 12月3日(水)-5日(金)に九州大学西新プラザにて, 研究集会「高信頼な理論と実装のための定理証明および定理証明器」を開催します. 皆様のご参加をお待ちしています. 日時：2014年 12月3日(水) 〜 12月5日(金) 場所：九州大学・西新プラザ (福岡市早良区西新2-16-23) http://bit.ly/QdaiNishijin 福岡空港から地下鉄で西新駅まで約20分, その後, 徒歩約10分. プログラム：詳細は未定(準備中)です. みなさまのご講演をお待ちしています. Adam Chlipala氏 (MIT, USA), Cyril Cohen 氏 (Univ. Gothenburg, Sweden) をお招きして, Coqおよび Ssreflect, MathCompに関する御講演を頂く予定です. 参加者と講演の数を大体把握しておきたいと思いますので，参加される方は 10月半ばまでに下の参加申し込みを下記メールアドレスまでお送りください．参加者には，できるだけ講演していただければと思います．申込み・問い合わせ先: tpp2014(a)imi.kyushu-u.ac.jp (溝口佳寛(九州大学)) URL: http://coop-math.ism.ac.jp/event/2014E04 (注. 作成途中です.「TPP2014 数学」で検索してみて下さい.) ------------------------------------------------------------------------- TPP 2014 参加申し込みお名前：ご所属：講演　：する／しない懇親会：参加する／参加しない講演する場合タイトル：（講演のタイトルが決まっていなければ，TBAでもかまいません．決まったらご連絡ください．）講演希望日: (○/×) 12/3 (○/×) 12/4 (○/×) 12/5 その他(ご意見/ご要望ありましたらお願いします): ------------------------------------------------------------------------- ========================================================================= Workshop: Theorem proving and provers for reliable theory and implementations (TPP2014) This is the call for participation for TPP2014, to be held on Dec. 3(Wed) - 5(Fri), 2014 at Kyushu University. Date: 2014/12/03 around 1pm to 12/05 around 3pm Venue: Nishijin Plaza, Kyushu University (2-16-23 Nishijin, Sawara-ku, Fukuoka City) http://bit.ly/QdaiNishijinPDF Invited Speakers: Adam Chlipala (MIT, USA) Cyril Cohen (Univ. Gothenburg, Sweden) If you are planning to attend the meeting, please send the information slip below to the indicated address by mid-October. Submission/questions to: 　　　tpp2014(a)imi.kyushu-u.ac.jp (Yoshihiro Mizoguchi) URL: http://coop-math.ism.ac.jp/event/2014E04 (Tentative Japanese HP. Revised English HP will be notified later.) ------------------------------------------------------------------------- TPP 2014 Registration Name: Affiliation: Will give a talk: Yes/No Will attend the party: Yes/No Title of the talk: (If it is not decided yet, TBA is OK.) Which date do you prefer to talk ? 12/3 (OK/NG) 12/4 (OK/NG) 12/5 (OK/NG) Requests for the organizer (if any): ------------------------------------------------------------------------- =========================================================================

1 0

Prof. Aart Middeldorp at NII Logic Seminar
by Makoto Tatsuta 17 Sep '14

17 Sep '14

Prof. Aart Middeldorp at NII Logic Seminar Date: September 22, 2014, 14:00--16:00 Place: National Institute of Informatics, Room 2005 (20th floor) 場所: 国立情報学研究所 20階 2005室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Prof. Aart Middeldorp (University of Innsbruck) Title: Proving AC Termination by Knuth-Bendix Orders Abstract: Equational theories that contain axioms expressing associativity and commutativity (AC) of certain operators are ubiquitous. Theorem proving methods in such theories rely on well-founded orders that are compatible with the AC axioms. In this talk we consider various definitions of AC-compatible Knuth-Bendix orders. The orders of Steinbach and of Korovin and Voronkov are revisited. The former is enhanced to a more powerful AC-compatible order and we modify the latter to amend its lack of monotonicity on non-ground terms. We present new complexity results and compare the various orders on problems in termination and completion. The talk is based on joint work with Nao Hirokawa, Sarah Winkler, and Akihisa Yamada. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

第49回 MLG 数理論理学研究集会のご案内
by Katsuhiko Sano 29 Aug '14

29 Aug '14

第49回 MLG 数理論理学研究集会のご案内 (重複してお受け取りの際はどうぞご容赦ください。) 北陸先端科学技術大学院大学の佐野勝彦と申します。少し先にはなりますが、2014年度MLG数理論理学研究集会（第49回）を下記の要領で開催いたします。多くの方のご講演・ご参加をお待ちしております。 ========================================= 第49回 MLG 数理論理学研究集会開催要領 ========================================= - 期間: 2014 年 12 月 5 日(金) 〜 12 月 7 日(日) - 場所: 山中温泉河鹿荘ロイヤルホテル（JR加賀温泉駅から車で約20分，加賀温泉駅から送迎あり） -- 〒922-0126 石川県加賀市山中温泉河鹿町ホ100 -- URL : http://www.daiwaresort.jp/kajikasou/ - 講演・宿泊申込締め切り: 2014 年 11 月 21 日（木） - 申し込みはこちらから --> http://goo.gl/RfZ5SE - ホームページ: https://sites.google.com/site/mlg2014kaga/ - 連絡先E-mail: mlg.logic.japan [at] gmail.com ============ 参加募集 ============ - 講演時間は原則40分を予定しています。 - 12月6日（土）の夜に懇親会を行います。 - 全日程参加の場合，参加費（宿泊代・食事代・会場代）は25000円前後になる予定です。 - ご講演をなさらなくても参加いただけます。山中温泉河鹿荘ロイヤルホテルで宿泊および食事をなさらない場合にも参加費（会場代）3000円をいただきます。 - 参加・講演申し込みは、http://goo.gl/RfZ5SE の registration form からお願い致します。世話人: 佐野勝彦〒923-1292 石川県能美市旭台1-1 北陸先端科学技術大学院大学情報科学研究科 MLG2014 に関するメールは，mlg.logic.japan [at] gmail.com まで。

1 0

再送：数学基礎論若手の会
by Satoru YOSHIDA 18 Aug '14

18 Aug '14

皆様重複して受け取られた場合はご容赦ください。数学基礎論若手の会2014のご案内です。数学基礎論を専攻する学生および若手研究者の研究交流を目的とする合宿形式の研究集会です．講演はオリジナルの成果発表に限らず，研究の途中報告や研究内容の紹介など幅広く募集しております．また，これから数学基礎論を勉強したいと思っている方のご参加も歓迎します．多くの方々のご参加およびご講演をお待ちしています．日程：11月19日（水）午後－21日（金）午前場所：鳥取市サイクリングターミナル砂丘の家（鳥取砂丘付近） http://www.city.tottori.lg.jp/www/contents/1198114185831/ 幹事：吉田聡（鳥取環境大学） satoru-y(a)kankyo-u.ac.jp ホームページ： http://misc.kankyo-u.ac.jp/~satoru-y/wakate14/ 今年度若手の会申込み要領については上記ホームページをご参照ください。 -- 吉田聡<YOSHIDA Satoru> 鳥取環境大学

1 0

ドメイン名の変更
by Atsushi Igarashi 13 Aug '14

13 Aug '14

kisoron-ml購読のみなさま，五十嵐＠京大％kisoron-ml管理人です． kisoron-ml のアドレスのドメイン名部分を変更いたします．旧) kisoron-ml(a)sato.kuis.kyoto-u.ac.jp 新) kisoron-ml(a)fos.kuis.kyoto-u.ac.jp 現在はどちらののアドレスでも投稿を受け付けておりますが， 2014年8月31日をもちまして旧アドレスを廃止いたします．不明な点があればお問い合わせください．どうぞよろしくお願いいたします． -- 五十嵐淳 (IGARASHI Atsushi) E-mail: igarashi(a)kuis.kyoto-u.ac.jp url: http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/

1 0

Kusatsu seminar
by Toshihiko Kurata 29 Jul '14

29 Jul '14

皆様，毎年行われています「ラムダ計算と論理の晩夏セミナー」について御案内させて頂きます．今年度は期間：9月21-25日場所：国立大学草津セミナーハウスで計画されていまして，詳細な情報は http://www.i.hosei.ac.jp/~kurata/2014LLS/ を御覧頂けたらと思います．申込・質問などの受付は倉田（法大）となっていますので何かありましたら遠慮なく御連絡下さい．それではよろしくお願いいたします． -- Toshihiko Kurata, Hosei University e-mail: kurata(a)hosei.ac.jp

1 0

数学基礎論若手の会2014のご案内
by YOSHIDA Satoru 17 Jul '14

17 Jul '14

kisoron-mlの皆様鳥取環境大学の吉田聡と申します。数学基礎論若手の会2014のご案内をさせて頂きます：数学基礎論を専攻する学生および若手研究者の研究交流を目的とする合宿形式の研究集会です．講演はオリジナルの成果発表に限らず，研究の途中報告や研究内容の紹介など幅広く募集しております．また，これから数学基礎論を勉強したいと思っている方のご参加も歓迎します．多くの方々のご参加およびご講演をお待ちしています．日程：11月19日（水）午後－21日（金）午前場所：鳥取市サイクリングターミナル砂丘の家（鳥取砂丘付近） http://www.city.tottori.lg.jp/www/contents/1198114185831/ 幹事：吉田聡（鳥取環境大学） satoru-y(a)kankyo-u.ac.jp ホームページ： http://misc.kankyo-u.ac.jp/~satoru-y/wakate14/ 今年度若手の会申込み要領については上記ホームページをご参照ください。 -- 吉田聡<YOSHIDA Satoru> 鳥取環境大学

2 1

モデル理論夏の学校2014＠筑波大学
by kota takeuchi 25 Jun '14

25 Jun '14

皆様、筑波大学の竹内耕太です。モデル理論夏の学校は毎年夏に開催されるモデル理論の研究集会です。今年は9月に筑波大学で開催されます。モデル理論ならびに関連分野に興味をお持ちの方はぜひご参加下さい。 (また講演希望者や学生を対象に一部旅費の援助も検討しています。必要に応じてご相談ください。) 竹内耕太 ------------------------------------------------------------------ モデル理論夏の学校2014 開催案内・参加募集ウェブページ：http://www.math.tsukuba.ac.jp/~kota/summerworkshop2014.html 日時：2014年9月14日（日）－16日（火）会場：筑波大学（つくばキャンパス）講演申込締切：8月31日（日）世話人連絡先：竹内耕太 kota(a)math.tsukuba.ac.jp 講演を希望される方は・タイトル・氏名・所属・希望時間（あれば）を竹内までメールにてお知らせください。参加に事前申し込みは必ずしも必要ありませんが、大まかな人数を把握するために事前に参加の旨連絡いただけるとうれしいです。竹内耕太（筑波大学）

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 23 Jun '14

23 Jun '14

皆様リーズ大学のJohn Stell先生の講演のお知らせです。ふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学研究科 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 (http://corcon.net/). Date: Friday 27 June, 2014, 15:30-17:00 Place: JAIST, 7F seminar room (I-75) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Dr. John Stell (University of Leeds, UK) Title: Bi-Intuitionistic Modal Logic and Hypergraphs Abstract: I will discuss motivations from spatial reasoning and mathematical morphology (as used in image processing) for the notion of a relation on a graph. I will show how the algebra of these relations is weaker than that of relations on a set. This leads to a generalization of relation algebras in which the Boolean algebra is replaced by a symmetric Heyting algebra. These relations can be used as the accessibility relations for a modal logic in which propositions are interpreted as subgraphs of a graph or more generally a hypergraph. --------------------------------------------------

1 0

春の数学会
by KASHIMA Ryo 13 Jun '14

13 Jun '14

日本数学会数学基礎論および歴史分科会会員の皆様、連絡責任評議員の鹿島です。春の学会（2014年3月15日(土)から3月18日(火)学習院大学）の一般講演申し込みが始まりました（オンライン講演申込締め切りは12月1日）。多くの発表をしていただけると嬉しいです。開催情報は以下をご覧下さい： http://mathsoc.jp/meeting/gakushuin14mar/ ＝＝＝＝＝＝＝＝＝＝【発表をされる方へのお願い】今回から新たに、　アブストラクトの最終的な印刷用PDFファイルの確認を　講演申し込み者本人が行うということになりました。具体的には12月24日（火）から12月27日（金）の短い期間に申込者本人が確認作業をする必要があるようです。詳細は次をご覧下さい： http://mathsoc.jp/meeting/gakushuin14mar/outline.html ----- 鹿島亮東京工業大学大学院情報理工学研究科数理・計算科学専攻 kashima(a)is.titech.ac.jp

2 2

The Second Taiwan Philosophical Logic Colloquium (2014 TPLC) Call for Papers
by Katsuhiko Sano 05 Jun '14

05 Jun '14

皆様、北陸先端科学技術大学院大学の佐野勝彦です。今年 10/24, 10/25 に台湾で開催される Logic Colloquiumについてご案内いたします。佐野勝彦 --- The Second Taiwan Philosophical Logic Colloquium (2014 TPLC) Call for Papers 24th (Fri.) -- 25th (Sat.) October, 2014 The Program for Logic, Mind and Methodology (LMM), Department of Philosophy, National Taiwan University, Taipei, Taiwan DEADLINE OF THE SUBMISSION OF ABSTRACTS: August 31st, 2014 DESCRIPTION OF THE COLLOQUIUM The 2014 TPLC is the second of the series of Taiwan Philosophical Logic Colloquium, which is one of two series of biennial conferences established since 2012 and based in The Program for Logic, Mind and Methodology (LMM), Department of Philosophy, National Taiwan University, Taiwan. (The other one is the series of Taiwan Metaphysics Colloquium, established since 2013.) Each event in these two series by and large runs in one/two days only. We usually invite one or two distinguished philosophers/logicians as keynote speakers and 3-4 distinguished scholars from Asian and Australasian regions together with several contributed papers. We hope that the establishment of these two series will make a rewarding and inspiring series of events so as to promote the development of metaphysics and philosophical logic in Asian area, especially in Taiwan. In particular, the aim of the series of Taiwan Philosophical Logic Colloquium is to bring together a group of logical-minded philosophers and a group of logicians with philosophical orientation. We intend, via the establishment of this series, to provide a forum for dialogues amongst philosophers and logicians with regard to a variety of significant issues and topics from philosophical and logical perspective, respectively. The scope of this series of colloquium will cover: philosophical logic (in a broad sense), non-classical logics, algebraic logic, all kinds of semantics/logics relating to philosophical concepts in metaphysics, epistemology, philosophy of language, philosophy of logic/mathematics, and their applications in computer science and cognitive science. KEYNOTE SPEAKERS FOR THE 2014 TPLC Robert Goldblatt, ``Admissible semantics for modal logic with quantifier'' (School of Mathematics, Statistics and Operations Research, Victoria University, New Zealand.) Hiroakira Ono, ``On interpolation properties'' (Japan Institute of Science and Technology (JAIST), Japan) INVITED SPEAKERS FOR THE 2014 TPLC Chen Bo (Peking University, China); Hanti Lin (Australia National University, Australia; UC Davis, USA) Fenrong Liu (Tsinghua University, China) Tomoyuki Yamada (Hokkaido University, Japan); SUBMISSION OF ABSTRACTS All researchers working on various aspects of philosophical logic are cordially invited to submit their abstracts by August 31st, 2014. Authors should submit an (extended) abstract at least about one page (A4 size, single space) but no more than four pages. Abstracts must be submitted as PDF files and sent to dmdeng(a)ntu.edu.tw (cc. Joshua S. S. [bookitchen(a)gmail.com.]) Each submission will be reviewed. The Colloquium is open to everyone, and practical info will be available soon on the website. SPECIAL OFFER FOR SPEAKERS FROM ABROAD Contributed papers from international scholars are highly appreciated. There will be a possibility of giving support of accommodation during the conference to speakers from abroad. Please take a contact with Syraya C. M. Yang (cmyang(a)ntu.edu.tw). However, it is strongly recommended that as long as you have decided to submit an abstract, please send us a note at your convenience as hotel-room preservation can be made the earlier the easier. POST-CONFERENCE PUBLICATION: We are planning to publish a post-conference proceedings for the 2014 TPLC once we get enough number of submissions of high quality. We have already taken a contact with editor-in-chief of LIAA book series concerning with this matter. The LIAA (``Logic in Asia'') is a new established publication project for a series of logic books from Springer. See http://www.springer.com/series/13080. If our project is approved, a post- conference proceedings will be published as a volume of LIAA. All authors of papers presented at the colloquium will be encouraged to submit a full version and the deadline of submission of manuscripts will be around February of 2015. All papers submitted will be refereed to high journal standards, and acceptance as a presentation is no guarantee that the post-conference paper will be published. The approval and the details of the post-conference proceedings will be announced later. ORGANIZATION COMMITTEE D. M. Deng, Y. I. Liang, C. J. Liau (The Institute of Information Science, Academia Sinica), E. M. Peng, H. C.Tsai (National Chung Cheng University), S. P. Tung (Chung Yuan Christian University), R. L. Wang, S. C. M. Yang (Chair), J. J. Yuann FFURTHER CONTACT: For any enquiry/information please contact: D. M. Deng (dmdeng(a)ntu.edu.tw) Joshua S. S. (bookitchen(a)gmail.com) Syraya C. M. Yang (cmyang(a)ntu.edu.tw)

1 0

Program of SLACS 2014 / 2014 Nonstandard Analysis Symposium
by YOKOYAMA Keita 20 May '14

20 May '14

皆様、北陸先端大の横山です。以前にもご案内いたしました2014年度のSLACS及び超準解析シンポジウムのプログラムを公開いたしました。 http://www.jaist.ac.jp/~y-keita/2014SLACS-NSA/speakers.html 27日には・斉藤正彦先生の特別講演、・小澤正直先生、蓮尾一郎先生の基調講演がございます。貴重な機会かと存じます、奮ってご参加ください。また、27日には両研究集会合同の懇親会を行います。お店のスペースの関係上、席の残りが少なくなっておりますので、参加をご検討の方はお早めにお申し込みください。どうぞよろしくお願いいたします。 For the information in English, please see the following web page. http://www.jaist.ac.jp/~y-keita/2014SLACS-NSA/index-e.html 以下、研究集会の情報です。 *************************** SLACS 2014 / 2014年度超準解析シンポジウム日時：5月26日（月）～5月28日（水）（但し、原則として、SLACSの講演は26,27日、超準解析シンポジウムの講演は27,28日とし、27日は一部交流形式を取る。）場所：東京工業大学大岡山キャンパス、西８号館Ｅ棟10階大会議室 ※合同懇親会を5月27日に行う予定です。ホームページ http://www.jaist.ac.jp/~y-keita/2014SLACS-NSA/index.html 27日には、2つの研究集会の交流の一環として、次の二つの基調講演を予定しております。・蓮尾一郎先生（東京大学、SLACSより）・小澤正直先生（名古屋大学、超準解析シンポジウムより）さらに、特別講演として、東京大学名誉教授の斉藤正彦先生より、超準解析学や周辺分野の日本における発展の歴史などについてお話をいただける予定です。 === 参加登録・講演の申し込みについて===================== 参加登録は、以下のフォームを横山までお送りください。送り先：y-keita(a)jaist.ac.jp ===以下フォーム=== 1. お名前 2. 所属 3. 参加日程 4. 懇親会(5月27日): 参加 / 不参加 5. 連絡先 E-mail 6. その他リクエスト等 ===以上フォーム=== ご登録されなくても当日の参加は可能ですが、準備の都合上できるだけ事前にご登録頂けますと助かります。また、懇親会につきましては、会場の状況次第で満席で受付を締め切る可能性があります。あらかじめご了承ください。 *************************** -- Keita Yokoyama y-keita(a)jaist.ac.jp

1 0

JAIST Logic Seminar Series
by Takako Nemoto 16 May '14

16 May '14

皆様インスブリア大学のMarco Benini 先生の講演のお知らせです。ふるってご参加ください。問い合わせ先：根元多佳子北陸先端科学技術大学院大学情報科学研究科 e-mail: t-nemoto(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: Thursday 22, May, 2014 15:30-17:00 Place: JAIST Collaboration Room 6 (I57-g) (Access:http://www.jaist.ac.jp/english/location/access.html) Speaker: Dr. Marco Benini Title: Point-free foundations of Mathematics Abstract: Is it possible to work with logical theories without assuming the existence of a universe where to interpret terms? This talk will positively answer to the above question in the case of first-order, intuitionistic-based theories by providing a class of models, defined inside Category Theory, such that they allow to interpret theories in a sound and complete way. Furthermore, the models explain the computational meaning of the corresponding theories via a semantic version of the Curry-Howard isomorphism. And their peculiar aspect is that they provide no universe where to interpret terms.

1 0

【講演募集の延長】SLACS 2014 / 2014 Nonstandard Analysis Symposium
by YOKOYAMA Keita 07 May '14

07 May '14

皆様、北陸先端大の横山です。繰り返しになりまして恐縮ですが、 2014年度のSLACS及び超準解析シンポジウムについて再度ご案内させていただきます。講演申し込みの締め切りを本日にしておりましたが、超準解析シンポジウムの方は講演スロットにまだかなりの余裕があり、 SLACSにつきましても、まだ若干の余裕がありますので、引き続き、スロットの許す限り、講演を募集いたします。ご参加・ご講演をよろしくご検討ください。横山 -------------------- 2014年度のSLACS及び超準解析シンポジウムを、以下の通り開催いたします。 http://www.jaist.ac.jp/~y-keita/2014SLACS-NSA/index.html どちらの集会も、例年とは時期が異なりますのでご注意ください。ご参加・ご講演をよろしくご検討ください。以下、研究集会の情報です。 *************************** SLACS 2014 / 2014年度超準解析シンポジウム日時：5月26日（月）～5月28日（水）（但し、原則として、SLACSの講演は26,27日、超準解析シンポジウムの講演は27,28日とし、27日は一部交流形式を取る。）場所：東京工業大学大岡山キャンパス、西８号館Ｅ棟10階大会議室 ※合同懇親会を5月27日に行う予定です。ホームページ http://www.jaist.ac.jp/~y-keita/2014SLACS-NSA/index.html 27日には、2つの研究集会の交流の一環として、次の二つの基調講演を予定しております。・蓮尾一郎先生（東京大学、SLACSより）・小澤正直先生（名古屋大学、超準解析シンポジウムより）さらに、特別講演として、東京大学名誉教授の斉藤正彦先生より、超準解析学や周辺分野の日本における発展の歴史などについてお話をいただける予定です。 === 参加登録・講演の申し込みについて===================== 参加登録・講演のお申し込みは、以下のフォームを横山までお送りください。送り先：y-keita(a)jaist.ac.jp 講演をお申し込みの方はお早めに申し込みをお願い致します。講演希望時間は30分程度、45分程度の2種類を準備する予定ですが、応募件数の都合上ご希望に添えない際はご容赦ください。 ===以下フォーム=== 1. お名前 2. 所属 3. 参加日程 4. 懇親会(5月27日): 参加 / 不参加 5. 連絡先 E-mail 6. その他リクエスト等以下講演をお申し込みの方 7. 講演希望カテゴリー: SLACS / 超準解析 / どちらでも（基本的に、SLACSの講演は26,27日、超準解析シンポジウムの講演は27,28日になります。） 8. 講演可能な日程: (可能な範囲で調整致します) 9. 講演希望時間: 30分程度 / 45分程度 / どちらでも 10. 講演タイトル: (未定の場合、決まり次第お願いします。) ===以上フォーム=== ご登録されなくても当日の参加は可能ですが、準備の都合上できるだけ事前にご登録頂けますと助かります。また、懇親会につきましては、会場の状況次第で満席で受付を締め切る可能性があります。あらかじめご了承ください。 *************************** 横山啓太 -- Keita Yokoyama y-keita(a)jaist.ac.jp

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Kisoron-ml