Kisoron-ml January 2012

kisoron-ml@fos.kuis.kyoto-u.ac.jp

2 participants
4 discussions

数学基礎論および歴史分科会総会
by KASHIMA Ryo 18 Jun '13

18 Jun '13

日本数学会数学基礎論および歴史分科会会員の皆様、連絡責任評議員の鹿島です。分科会総会の代わりのメールです。ご意見等がありましたらお知らせください。【１】今年の数学基礎論サマースクールはモデル理論がテーマで米田郁生さんが幹事をしてくださります。数学基礎論若手の会の幹事は酒井拓史さんがやってくださると聞きました。例年通り、数学会本部から分科会へ支給される補助金を１万円ずつこの二つの会に出したいと思います。【２】上記の他にも各種研究集会の予定があると思います。分科会ホームページや数学通信に載せていきますので、幹事の方は是非とも情報をお知らせください。５月発行の数学通信に載せるためには、　４月１５日（金）までに鹿島まで情報をお寄せくださるよう、お願いいたします。【３】『数学』編集委員は、現在は池田宏一郎さんですが、４月から鈴木登志雄さんに交代します。【４】現在の分科会運営委員は次のようになっています。（敬称略、括弧内は代表分野、順番は任期の早い順）三宅克哉（歴史）倉田俊彦（計算機科学）高瀬正仁（歴史）山下秀康（超準解析）只木孝太郎（帰納的関数論及び計算理論）桔梗宏孝（モデル理論）安東祐希（証明論）依岡輝幸（集合論）志村立矢（非古典論理）【５】分科会選出評議員は次の通りです：鹿島亮（連絡責任評議員）隈部正博（受賞候補推薦委員）分科会に対するご意見ご質問は評議員またはお近くの運営委員までお寄せください。【６】 3月20日に行われた総会・評議員会での審議決定事項等のうち、重要なものを報告します。 (a) 今後の年会および秋季総合分科会の予定： 9月28(水)〜10月1日(土) 信州大学 2012年３月東京理科大学 2012年９月九州大学 (b) 新理事長に宮岡洋一氏が選出されました。 (c) 早稲田での年会は中止になりましたが、「アブストラクト集が発行されたことによって成立したこととします」だそうです。つまり、今回講演を申し込んだ人はそれを各自の発表業績として数えてよい、ということです。アブストラクト集は数学会本部でとりまとめて今後希望者に販売するそうです。今回講演を申し込んだ人が同じ内容の講演を秋または来春の学会で行うことも可能だそうです。 (c)について、さらに他にも数学会本部からのお知らせは数学会ホームページ： http://mathsoc.jp/ に随時掲載されますので、各自でご確認お願いいたします。【以上】 ----- 鹿島亮東京工業大学大学院情報理工学研究科数理・計算科学専攻 kashima(a)is.titech.ac.jp

1 5

NII Type Theory Workshop
by Makoto Tatsuta 31 Jan '12

31 Jan '12

Seventh NII Type Theory Workshop Date: February 6, 2012, 13:00--17:00 Place: National Institute of Informatics, Room 2005 (20th floor) 場所: 国立情報学研究所 20階 2005室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/introduce/access1-j.shtml) Program: 13:00--13:30 Daisuke Kimura (National Institute of Informatics) Title: A generalized modal lambda calculus 13:30--14:00 Kazuyuki Asada (National Institute of Informatics) Title: Semantics of Multi-rooted Graph with Ordered Branch 14:00--14:20 Tea Break 14:20--15:00 Makoto Tatsuta (National Institute of Informatics) Title: Type Inference for Bimorphic Recursion 15:00--15:40 Yukiyoshi Kameyama (University of Tsukuba) Title: Pseudo-Classical Modal Logic for Staged Computation 15:40--16:00 Tea Break 16:00--17:00 Stefano Berardi (Torino University) Title: A Game Semantic for various Subclassical Logics Abstracts: ---------------------------------------------------------------------- Daisuke Kimura (National Institute of Informatics) Title: A generalized modal lambda calculus Abstract: In this talk, we introduce a lambda calculus with modal types. The types of this system contain information of possible worlds explicitly. This information can be considered as a position which is an abstraction of time or place. The feature of our calculus is that we can change the property of modalities by changing information about the relationship between positions. The aim of our research is the following: (1) To clarify the computational meaning of necessity and possibility modal operators. (2) To give a uniform framework that can treat several calculi with modal types. ---------------------------------------------------------------------- Kazuyuki Asada (National Institute of Informatics) Title: Semantics of Multi-rooted Graph with Ordered Branch Abstract: Buneman et al. introduced a graph transformation language UnCAL, where graph has bisimilarity semantics. There structural recursion plays an important role, and in order to define it, they introduced multi-rooted graph and its algebraic representation. In this talk we give coalgebraic semantics for multi-rooted graph, and see that such final coalgebras has some call-by-value structure. Then we introduce a CBV equational theory. Next we modify the results of graph with un-ordered branch to that with ordered branch, which is important for application to XML. For this ordered graphs, bisimilarity is defined in some subtle way, but we can use the ordered version of above CBV equational theory for reasoning of the bisimilarity between ordered graphs. ---------------------------------------------------------------------- Makoto Tatsuta (National Institute of Informatics) Title: Type Inference for Bimorphic Recursion Abstract: This talk proposes bimorphic recursion, which is restricted polymorphic recursion such that every recursive call in the body of a function definition has the same type. Bimorphic recursion allows us to assign two different types to a recursively defined function: one is for its recursive calls and the other is for its calls outside its definition. Bimorphic recursion in this talk can be nested. This talk shows bimorphic recursion has principal types and decidable type inference. Hence bimorphic recursion gives us flexible typing for recursion with decidable type inference. This talk also shows that its typability becomes undecidable because of nesting of recursions when one removes the instantiation property from the bimorphic recursion. This is a joint work with Ferruccio Damiani. ---------------------------------------------------------------------- Yukiyoshi Kameyama (University of Tsukuba) Title: Pseudo-Classical Modal Logic for Staged Computation Abstract: In this talk, we study a pseudo-classical modal logic, which corresponds to the staged calculus with control operators introduced by our earlier work. Staged computation is a means for run-time code generation, and has been proved useful in improving efficiency and maintainability of software. We are interested in the use of control operators in staged computation, since they play an essential role to avoid the code duplication problem. Combining a staged calculus with control operators in a naive way results in an unsound calculus, and we need a restriction on the typing rule for lambda. We show that this restriction has a logical counterpart similar to Nakano's catch/throw calculus. ---------------------------------------------------------------------- Stefano Berardi (Torino University) Title: A Game Semantic for various Subclassical Logics Abstract: In this talk we describe the state of the art of game semantics for Logic and lambda-calculus, and the motivations for having a game semantics. Then we define a game semantic for Intuitionism extending both Coquands and Hyland-Ongs game semantics. The semantics refines a paper of TLCA 2007. We have two kind of results: (1) (Soundness and Completeness) The recursive winning strategy of our game semantics are isomorphic to the cut-free proofs of some variant of HA-omega (Infinitary Intuitionistic Arithmetic) (2) (Cut Elimination) Any debate between two terminating strategies terminates. This is an ongoing joint work with M. Tatsuta. ---------------------------------------------------------------------- 連絡先龍田真 (国立情報学研究所)

1 0

佐藤雅彦先生最終講義の御案内
by Koji Nakazawa 25 Jan '12

25 Jan '12

kisoron-mlのみなさま，（重複の場合はご容赦ください）京都大学の中澤です．この3月をもって定年を迎えられる佐藤雅彦先生の最終講義が下記のとおり行なわれますので，この場をお借りしまして，お知らせいたします． ---------------------------------------------------------------------- 各位小林茂夫教授・佐藤雅彦教授・後藤修教授最終講義および懇親会のご案内拝啓時下ますますご健勝のこととお喜び申し上げます。さてこの度、知能情報学専攻小林茂夫教授，佐藤雅彦教授，後藤修教授におかれましては、本年３月 31日をもって定年を迎えられ京都大学を退職されることとなりました。つきましては、三教授による最終講義および懇親会が行われますので、下記の通りご案内申し上げます。敬具記 1. 最終講義日時: 平成 24 年 3 月 16 日 (金) 午後 13:00 〜 18:00 会場: 京都大学百周年時計台記念館国際交流ホールI http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (3番の建物) 13:00〜14:30 佐藤雅彦教授「情報学の内と外〜世界と言語の関係〜」 14:45〜16:15 後藤修教授「ＤＮＡ＝高分子＋情報」 16:30〜18:00 小林茂夫教授「物理世界と感覚世界」 2. 懇親会日時: 平成 24 年 3 月 16 日 (金) 午後 18:45 〜 20:45 (受付: 18:15 〜) 会場: 京都大学百周年時計台記念館国際交流ホールIII http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (3番の建物) 会費: 一般 8,000円，学生 4,000円 [事前登録] final-lec(a)sato.kuis.kyoto-u.ac.jp までお名前: ご所属: 佐藤教授最終講義 (ご出席・ご欠席) 後藤教授最終講義 (ご出席・ご欠席) 小林教授最終講義 (ご出席・ご欠席) 懇親会 (ご出席・ご欠席) をお知らせください． (事前登録は必須ではありませんが、特に懇親会に関しまして参加者数を把握するため、事前登録にご協力をお願い致します。) 平成24年1月吉日京都大学大学院情報学研究科知能情報学専攻長黒橋禎夫小林教授・佐藤教授・後藤教授最終講義および懇親会準備会 final-lec(a)sato.kuis.kyoto-u.ac.jp

1 0

Prof. Kwangkeun Yi Lecture at NII Logic Seminar
by Makoto Tatsuta 04 Jan '12

04 Jan '12

Prof. Kwangkeun Yi Lecture at NII Logic Seminar Date: January 10, 2012, 15:00--17:00 Place: National Institute of Informatics, Lecture Room 1208 (12th floor) 場所: 国立情報学研究所 12階 1208室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/introduce/access1-j.shtml) Speaker: Prof. Kwangkeun Yi (Seoul National University) Title: Static Analysis of Multi-Staged Programs via Unstaging Translation Abstract: Static analysis of multi-staged programs is challenging because the basic assumption of conventional static analysis no longer holds: the program text itself is no longer a fixed static entity, but rather a dynamically constructed value. This article presents a semantic-preserving translation of multi-staged call-by-value programs into unstaged programs and a static analysis framework based on this translation. The translation is semantic-preserving in that every small-step reduction of a multi-staged program is simulated by the evaluation of its unstaged version. Thanks to this translation we can analyze multi-staged programs with existing static analysis techniques that have been developed for conventional unstaged programs: we first apply the unstaging translation, then we apply conventional static analysis to the unstaged version, and finally we cast the analysis results back in terms of the original staged program. Our translation handles staging constructs that have been evolved to be useful in practice (typified in Lisp's quasi-quotation): open code as values, unrestricted operations on references and intentional variable-capturing substitutions. This article omits references for which we refer the reader to our companion technical report. This is a joint work with Wontae Choi, Baris Aktemur, and Makoto Tatsuta. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Kisoron-ml January 2012