Logic-ml

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

1792 discussions

Kobe Colloquium on Logic, Statistics and Informatics, January 27 (Monroe Eskew)
by Joerg Brendle 25 Jan '15

25 Jan '15

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。日時：2014年1月27日（火）13:20-14:50 講演者：Monroe Eskew （筑波大学）場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室） ============================================================ 題目： A global version of Chang’s conjecture アブストラクト： In the 80s, Foreman showed the consistency of (aleph_{n+1},aleph_n) —>> (aleph_{m+1},aleph_m) holding simultaneously for all natural numbers n > m, starting from a 2-huge cardinal. He asked whether a global version of Chang’s conjecture is consistent. We answer this, showing that it is consistent from the same hypothesis that for all pairs of regular cardinals mu < kappa, (kappa^+,kappa) —>> (mu^+,mu). The method uses a relatively simple forcing iteration, and it answers some technical questions raised by Shioya. We also discuss some related issues about singular cardinals. ============================================================ 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm

1 0

JSPS-NUS Joint Workshop in Logic
by Tanaka Kazuyuki 25 Jan '15

25 Jan '15

JSPS-NUS二国間共同研究のロジック・ワークショップのご案内シンガポールとの二国間交流事業（代表：田中、Chong）の一環として下記の研究会を開催致します。 Workshop in Mathematical Logic and Foundations of Mathematics 日程：2015年3月6日(金) から3月8日(日) まで場所：金沢しいのき迎賓館および金沢東急ホテルこのワークショップは主に共同研究のメンバーによって行われるものですが、ご関心のある方は一般からもご参加いただけます。但し、会場準備の都合上事前登録者に限りますので参加希望の方は SendaiLogic[at]math.tohoku.ac.jp （締切２月８日）までご連絡ください。下記のページで＜英語＞でもご案内しております。 http://www.math.tohoku.ac.jp/~tanaka/kanazawa2015.html よろしくお願いします。　東北大学　田中一之コンタクト：　SendaiLogic[at]math.tohoku.ac.jp

1 0

『第２回山陰基礎論・解析学研究集会』の御案内
by Horihata Yoshihiro 23 Jan '15

23 Jan '15

皆様米子高専の堀畑です．明日と明後日に米子で件名の研究会を開きます．ホームページ https://sites.google.com/site/yonagonctmath/slas2015 参加自由です．よろしくお願いいたします．参加者リスト阿部吉弘（神奈川大学）池上大祐（神戸大学）薄葉季路（神戸大学）嘉田勝（大阪府立大学）木原貴行（ＪＡＩＳＴ）熊本真一郎（金沢大学）倉橋太志（木更津高専）古清水大直（米子高専）小林玉青（米子高専）小浪吉史（島根大学）静間荘司（大阪府立大学）柴田孝祐（米子高専，建築学科５年）高木啓行（信州大学）竹内耕太（筑波大学）根元多佳子（ＪＡＩＳＴ）濱田裕康（佐世保高専）樋口幸治郎（千葉大学）吉居啓輔（沖縄高専）吉田聡（鳥取環境大学）米子高専・数学同好会学生３人世話人：堀畑佳宏 -- 米子工業高等専門学校教養教育科・数学〒683-8502 鳥取県米子市彦名町4448 Tel: 0859-24-5075 E-mail: horihata(a)yonago-k.ac.jp

1 0

Re: [logic-ml] メーリングリストへの配信願い
by Atsushi Igarashi 21 Jan '15

21 Jan '15

logic-ml のみなさま，五十嵐＠logic-ml管理人です．成蹊大学・理工学部・情報科学科の山本様からの依頼での代理投稿です． ---------------------------------------------------------- logic-ml の皆様，成蹊大学・理工学部・情報科学科の山本と申すものです．以下のように，当学科で助教の公募を行っています．募集期間が短く申し訳ありませんが，ご関心のある方々の応募をお待ちしております． 1. 募集人員：助教１名 (任期付き) 2. 所属：理工学部情報科学科 3. 専門分野：計算機科学・情報科学における理論分野全般 4. 着任時期：２０１５年５月１日（金） 5. 応募締切：２０１５年２月１４日（土）（必着）詳細は，下記 URL をご参照下さい． http://www.seikei.ac.jp/gakuen/recruit/teacher/university.html 以上．

1 0

PPL2015参加登録開始がご案内：第17回プログラミングおよびプログラミング言語ワークショップ
by Kazutaka Matsuda 16 Jan '15

16 Jan '15

logic-ml関係者の皆様，東京大学の松田です．複数受け取られた場合はご容赦ください． 3月4日（水）から3月6日（金）に道後温泉で開催される第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015) の参加登録を開始いたしましたで，そのご案内をお届けいたします．今回は， * 橋本和幸 (NVIDIA. 元日本シンボリックス株式会社) 「1980年代のLispマシンSymbolicsとその開発環境Genera 付属：NVIDIA GPUによる超並列コンピューティング」 * Chung-Kil Hur (Seoul National University) 「Formal C semantics and LLVM compiler validation」の二件の招待講演を予定しております．多くの方々のご参加をお待ちしております．参加登録の案内ページは http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/registration/ です．参加登録の締切は2月17日（火）です．どうぞお早めのご登録をお願い致します．今年は昨年と異なり，*三日目は全日開催*となります．ご注意ください．また，カテゴリ2（国外既発表論文），4（サーベイ・チュートリアル）の申し込みは 2015年1月23日(金) 17:00 (JST) まで，カテゴリ3（ポスター・デモ発表）の申し込みは 2015年2月6日(金) 17:00 (JST) まで受け付けております．こちらも http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ をご参照の上，投稿をご検討いただけますと幸いです． -------------------------------------------------------------------------- 第17回プログラミングおよびプログラミング言語ワークショップ（PPL2015） http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ 参加登録のご案内主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2015年3月4日(水)～3月6日(金) 会場: 愛媛県松山市道後温泉「道後プリンスホテル」 http://www.dogoprince.co.jp/ PPL2015は、プログラミングおよびプログラミング言語に関する研究者が一堂に会し、最新の研究成果の発表、および新たな研究課題についての討論やアイディア交換等を行うことを目的とした、合宿形式のワークショップです． ====================================================================== 参加登録ならびに宿泊予約を2月17日(火)まで日本旅行のWebサービスにて受け付けております． http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/registration/ をご参照いただき，ご登録ください．問い合わせ先：ppl2015-oc [at] kb.is.s.u-tokyo.ac.jp （[at]を@に置き換えてください） ====================================================================== プログラム委員会青戸等人東北大学浅田和之東京大学岩崎英哉電気通信大学鵜川始陽高知工科大学馬谷誠二京都大学 [プログラム共同委員長] 大岩寛産業技術総合研究所亀山幸義筑波大学河内谷清久仁日本IBM 久野靖筑波大学木村大輔国立情報学研究所宋剛秀神戸大学塚田武志 University of Oxford 中田景子 FireEye DresDen 浜名誠群馬大学 [プログラム共同委員長] 平井洋一 FireEye Dresden 平石拓京都大学藤田憲悦群馬大学星野直彦京都大学増原英彦東京工業大学渡部卓雄東京工業大学組織委員会松田一孝東京大学 [組織委員長] 浜名誠群馬大学 [プログラム共同委員長] 馬谷誠二京都大学 [プログラム共同委員長] 末永幸平京都大学上野雄大東北大学海野広志筑波大学木村大輔国立情報学研究所 [ポスターセッション幹事] --------------------------------------------------------------------------

1 0

Gilles Dowek教授講演会　１月１６日金曜日　三田ロジックセミナー
by Mitsuhiro Okada 14 Jan '15

14 Jan '15

次のようなセミナートークを予定しておりますのでご案内させていただきます。参加自由です。(日時が次のように変更しています。Please note that　the date/time changed as follows.) 　　　　　　　　慶應義塾大学文学部哲学専攻岡田光弘 ------------------------------ Mita Logic Seminar Jan.16th (Fri) 13:00-14:30 Place: Basement B1 , Meeting Room #3, North Building, Mita campus, Keio University　(Campus Map http://www.keio.ac.jp/en/maps/mita.html) １月１６日金曜日　１３時ー１４時半, 慶應義塾大学三田キャンパス北館地下一階第３会議室　(キャンパスマップhttp://www.keio.ac.jp/ja/access/mita.html） Speaker; Gilles Dowek, INRIA, France Title: Real numbers, chaos, and the principle of a bounded density of information Abstract: Two definitions of the notion of a chaotic transformation are compared: sensitivity to initial conditions and sensitivity to perturbations. Only the later is compatible with the idea that information has a finite density. 連絡先：思考と行動判断の研究拠点事務局（logic(a)abelard.flet.keio.ac.jp) ------------

1 0

PPL2015 ポスター発表申込み締切日訂正
by Makoto Hamana 13 Jan '15

13 Jan '15

皆様、すみませんです、先ほどご案内したPPL2015の案内メールのポスター・デモ発表申込み締切り日に間違いありましたので訂正させていただきます。 [訂正] カテゴリ3（ポスター・デモ発表）締切は 2015年2月6日(金) 17:00 (JST) です。カテゴリ4(サーベイ・チュートリアル)の方は1月23日〆で正しいです。 PPL 2015 Webページ http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ にあるものが正式な情報です。お騒がせして申し訳ありません。どうぞよろしくお願いいたします。 -- 浜名　誠群馬大学理工学府電子情報部門 http://www.cs.gunma-u.ac.jp/~hamana/

1 0

CFP: PPL2015 サーベイ・チュートリアル、ポスター発表募集
by Makoto Hamana 13 Jan '15

13 Jan '15

皆様、群馬大学の浜名です。来年3月に愛媛県松山市道後温泉で開催される第17回プログラミングおよびプログラミング言語ワークショップ PPL'15 2015年3月4日(水)〜3月6日(金) http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ のサーベイ・チュートリアル、ポスター発表申込みの案内をさせていただきます。 * サーベイ・チュートリアル発表 (カテゴリ4）は、今年のPPLからの試みで、プログラミング言語分野の学生、研究者に役立つようなサーベイ・チュートリアル発表を広く募集します。プログラミング言語理論も実装も歴史が深くなってきて、自分の特定専門分野の事は知っていても、なかなか他の小分野の事はよく知らないという事が多くなってきました。そこでプログラミング言語に関わる様々な理論、応用の小分野間の相互理解と全体の底上げとなる事を目指し、設置しました。既発表・未発表の別を問いません(申込みは簡単なアウトラインの提出のみ)。既存発表の解説論文、教科書、セミナーや講義での資料、経験などお持ちの方はそれを用いていただくのも便利かと思います。 - ある専門分野の事を皆にもっと知ってもらいたい！ - 難しい分野と言われているがアイデアはそんなことないから解説したい。 - 現在隆盛を誇っている分野はこんな風に発展してきた。あまり知られていないが自分の専門性から解説したい。 - 解説論文を出版したけど、これを発表で話したことはないな… - 自分もやってる活発な〇〇分野の研究動向をまとめたいけどなかなかきっかけがない。これを機にまとめようか。などいろいろパターン、動機はあるかと思います。上記どれか当てはまるような方、もちろんそれに限らず、ぜひ申込みいただければと思います。通常発表と同様の30分での発表を予定していますが、採択件数によっては発表者との相談で少し時間延長もできるかもしれません。通常研究発表とは違い、ある程度確立した分野の話、専門家の方にお願いできればと思っております。PPLへの関連および関連研究への言及をもとに採録を判定いたします。 * ポスター・デモ発表 (カテゴリ3)は例年盛況な2時間程度のセッション内でのポスター発表またはデモ発表です。既発表・未発表の別を問いません。今年はポスター賞も設置しました。申込み多数の場合はプログラム委員会での選考により採否を決定します。締切はどちら(カテゴリ3,4)も、来週末 2015年1月23日(金) 17:00 (JST) ですので、ぜひ申込みをご検討ください。詳しい申込み方法などは http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ ご参照ください。 -- 浜名　誠群馬大学理工学府電子情報部門 http://www.cs.gunma-u.ac.jp/~hamana/

1 0

KusatsuSeminar3/16--20
by Fujita Kenetsu 13 Jan '15

13 Jan '15

皆様，『ラムダ計算と論理の早春セミナー』のご案内日程：2015年3月16日(月) 午後5時から3月20日(金) 正午まで場所：国立大学草津セミナーハウス　　　〒377-1711 群馬県吾妻郡草津町大字草津字白根737 詳細：http://www.cs.gunma-u.ac.jp/~fujita/2015.03LLSinKusatsu.htm 申込・質問などは藤田（群馬大学）までご連絡をお願いします．興味をお持ちのみなさまのご参加をお待ちしております． ----------- 群馬大学　藤田憲悦

1 0

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

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml