Logic-ml

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

1792 discussions

数学基礎論若手の会2024開催のお知らせ
by 樋口幸治郎 24 Sep '24

24 Sep '24

皆様、日本大学の樋口幸治郎と申します。数学基礎論若手の会 2024 の開催 (対面で実施) をご案内いたします。数学基礎論若手の会は数学基礎論を専攻する学生および若手研究者の研究交流を目的とする研究集会です。講演はオリジナルの成果発表に限らず、研究の途中報告や研究内容の紹介など幅広く募集しております。また、これから数学基礎論を勉強したいと思っている方のご参加も歓迎します。 — 開催要領 — 日程：2024 / 10 / 12（土）～ 14（月, 祝日）会場：郡山市青少年会館（福島県郡山市大槻町字漆棒82番地）世話人：樋口幸治郎（日本大学）ウェブサイト： https://sites.google.com/view/mlwakatenokai2024/%E3%83%9B%E3%83%BC%E3%83%A0 参加申込み期限：2024 / 9 / 27 (金) 参加申込み(Googleフォーム)：https://forms.gle/kPSSzGkjNwH8RQE98 講演希望の方は、上記フォームの提出後、講演タイトル・アブストラクトのtexファイルを世話人へメールで送ってください。開催時期が近づきましたら、再度お知らせいたします。多くの皆様のご参加をお待ちしております。樋口幸治郎 (日本大学工学部)

1 2

公募情報
by Makoto Fujiwara 20 Sep '24

20 Sep '24

皆様東京理科大学の藤原誠です．本学理学部第一部応用数学科にて来年度4月着任予定の助教（任期制）2名及び准教授1名の公募を行っております． <https://www.tus.ac.jp/recruitment/teacher-list/> [recruiter_omg.png] 教員・研究員公募｜東京理科大学｜東京理科大学<https://www.tus.ac.jp/recruitment/teacher-list/> tus.ac.jp<https://www.tus.ac.jp/recruitment/teacher-list/> 応募締切は9月30日(月)です．もしよろしければ応募をご検討下さい．また，お近くに適任の方がいらっしゃればご紹介いただければ幸いです．どうぞよろしくお願いいたします． ---------------------------------------------------------- 藤原誠 (Makoto FUJIWARA) 東京理科大学理学部第一部応用数学科助教 E-mail: makotofujiwara(a)rs.tus.ac.jp<mailto:makotofujiwara@rs.tus.ac.jp> ----------------------------------------------------------

1 0

【発表募集】第151回プログラミング研究発表会（PRO-2024-3）
by Sosuke MORIGUCHI 20 Sep '24

20 Sep '24

※重複してお受け取りの場合はご容赦ください．皆様東京工業大学の森口と申します．情報処理学会第151回プログラミング研究発表会（PRO-2024-3）の延長した発表申込の締め切りが明日（9/20）になりましたので，ご案内させていただきます．ご検討のほどよろしくお願いいたします． ==== 情報処理学会第151回プログラミング研究発表会発表募集 https://sigpro.ipsj.or.jp/pro2024-3/ 日時：2024年11月12日(火)〜11月13日(水) 会場：東京科学大学（9月まで東京工業大学）大岡山キャンパス　　　およびオンラインのハイブリッド開催を予定参加費：無料発表申込締切：2024年9月13日（金）→2024年9月20日（金）（延長しました）投稿論文原稿提出締切：2024年10月7日（月）発表予稿提出締切：2024年11月08日（金）プログラミング研究会（PRO）は， * プログラミング言語の設計，処理系の実装 * プログラミングの理論，基本概念 * プログラミング環境，支援システム * プログラミング方法論，パラダイム * これらを応用したシステムの開発事例 * その他，プログラミングに関する面白い話題を対象とした研究発表の場です．研究会と密接にリンクした論文誌を1998年度から毎年3〜4回のペースで発行しており，研究発表会での発表内容を論文誌に投稿することができます．発表申込時に投稿を希望し投稿締切までに原稿が提出されている論文が査読の対象となります．採否は研究発表会からおおむね 3週間ほどで迅速に決定されます．論文誌への投稿を希望しない発表も歓迎します． 1件あたりの発表時間は45分（発表25分，質疑20分）です．通常の発表に加え，「短い発表」も募集します．「短い発表」の発表時間は30分（発表20分・質疑10分）です．発表内容は通常の発表と同様ですが，特に，萌芽的なアイデアの提示，進行中の研究の途中報告，システム開発経験や興味深いプログラミング技法の紹介，開発したツールやソフトウェアの紹介などを「短い発表」として歓迎します．発表資料は数ページ程度の短いもので結構です．ただし，「短い発表」の論文誌への投稿はできません．英語論文の投稿も歓迎します．2015年度以降，英語論文が採録された場合，その論文の正本は英語論文誌JIPに掲載されます．また，和文論文を採録決定後に英語化し英語論文として掲載する試みを行っています．英語論文の投稿をご検討の方は以下のアナウンスをご覧ください． https://sigpro.ipsj.or.jp/sigtra4/ 「5．英文論文誌JIPとの連携」「6. 和文論文の採録後の英語化」多くの発表ならびに論文投稿をお待ちしております．担当者：森口草介（東京工業大学），緒方一則（日本IBM）問い合わせ先：chiguri(a)c.titech.ac.jp

1 0

ワークショップのご案内（仙台・9/21）
by Hitoshi Omori 17 Sep '24

17 Sep '24

皆様東北大学の大森です。直前の案内となり恐縮ですが、以下の通りワークショップを開催いたします。 ===== ・日時：9月21日(土)10:00〜・場所：東北大学大学院情報科学研究科 310号室・講演者（敬称略）： *石原哉 (東邦大学), *根元多佳子 (東北大学), *仁木哲 (ルール大学), *豊岡正庸 (北海道大学). ・題目などの詳細は以下のウェブサイトをご覧ください。 https://sites.google.com/view/llal-at-gsis/meetings/llalgsis-4 ===== どうぞよろしくお願いいたします。大森仁

1 0

【論文/発表募集】第27回プログラミングおよびプログラミング言語ワークショップ (PPL 2025)
by Soichiro Hidaka 17 Sep '24

17 Sep '24

皆様， PPL 2025 プログラム共同委員長の一人の日高です．来年（2025）の 3/5〜7 にホテル明山荘にて開催予定の PPL 2025 の論文/発表募集をお送りいたします． PPL 2025 では，理論・実装を問わず，プログラミングおよびプログラミング言語に関する発表・論文を広く募集しております．どうぞ，発表・投稿をご検討いただけますと幸いです． PPL 2025 プログラム共同委員長（ppl2025-pc-chairs[at]easychair.org）塚田武志（千葉大学）日高宗一郎（法政大学） ================================================ 第27回プログラミングおよびプログラミング言語ワークショップ (PPL 2025) 論文募集/発表募集主催：日本ソフトウェア科学会プログラミング論研究会日程：2025年3月5日（水）-- 3月7日（金）会場：ホテル明山荘 URL ：https://jssst-ppl.org/workshop/2025/ ** 重要な日程 ** カテゴリ1：発表申込締切 2024年12月23日（月）17:00 (JST) 論文提出締切 2025年 1月 6日（月）17:00 (JST) 採否通知　　 2025年 1月29日（水）カテゴリ2：発表申込締切 2025年 1月20日（月）17:00 (JST) 採否通知　　 2025年 1月30日（木）カテゴリ3：発表申込締切 2025年 1月31日（金）17:00 (JST) 採否通知　　 2025年 2月 3日（月）カテゴリ4：発表申込締切 2025年 1月20日（月）17:00 (JST) 採否通知　　 2025年 1月30日（木） ** PPL 2025 の開催形式について ** PPL 2025 は合宿形式での対面での開催を予定しています．PPL 2023 では大学におけるハイブリッド開催，PPL 2024 ではコンベンションセンターによるハイブリッド開催と，COVID-19 状況下において PPL は様々な開催方法が試みられてきました．PPL 2025 では，会場確保を含めた様々な要因を考慮した結果，過去の合宿形式に近い形態での開催を試みることにしました．対面での開催とするのは，PPL 2025 を以前の PPL と同様にカジュアルかつインフォーマルな意見交換や交流の場にするためであり，発表者にも対面でご参加いただくことを考えております．オンラインへの提供の有無は現在検討中です． ** PPL 2025 とは ** PPL 2025 は，プログラミングとプログラミング言語に関連する幅広い分野の研究者・技術者・学生が一堂に会し，最新の研究成果や新たな研究課題の提案・討論・アイディア交換を行うことを目的とした研究集会です．代表的なトピックは以下のようなものですが，これらに限らず，プログラミングやプログラミング言語に関する内容であれば，基礎理論・実装技術の研究からソフトウェアやツールの実現に至るまで，幅広く受け入れます．基礎理論：意味論，ラムダ計算，型理論，項書き換え，形式論理と証明，形式　　　　　言語とオートマトン，圏論，チューリング機械，アルゴリズムなど言語デザイン：各種プログラミングパラダイム（オブジェクト指向・関数型・　　　　　　　論理型・アスペクト指向，その他あらゆるパラダイムを含む），　　　　　　　モジュール化，メタプログラミング，並行・並列・分散計算，　　　　　　　型システム，言語や言語システム等の相互運用，領域限定言語　　　　　　　など言語処理系技術：コンパイラ，インタプリタ，実行時システム，仮想機械，プ　　　　　　　　ログラム最適化，プログラム解析，プログラム変換，メモリ　　　　　　　　管理などプログラミング補助：プログラム検証器，デバッガ，プロファイラ，統合開発　　　　　　　　　　環境，プログラム合成，リファクタリングなどケーススタディ：ソフトウェア開発報告，プログラミング技法，ツールの紹介　　　　　　　　など応用：システムソフトウェア，Webシステム，データベースシステム，数値計　　　算，ユーザーインタフェース，セキュリティ，プログラミング教育，人　　　工知能・機械学習など ** 発表募集カテゴリ ** 以下の4カテゴリの研究発表を募集します．カテゴリ1：国内外未発表論文カテゴリ2：国際既発表論文カテゴリ3：ポスター・デモ発表カテゴリ4：サーベイ・チュートリアルカテゴリ1 では，国内外で未発表の論文発表を募集します．PPL での議論をもとに研究を発展させ，国際会議や学術論文誌への投稿につなげることを奨励しています．そのため，予稿集の配布は参加者のみへの限定的なものとします．参加者相互で実りある議論ができるような，発展途上の研究を特に歓迎します．また国際会議等との同時投稿も（もう一方の投稿先が認めている限り）認められる場合があります．カテゴリ1の趣旨に照らして認めるか否かを個別に判断しますので，発表申し込みに先立ってppl2025-pc-chairs[at]easychair.org に問い合わせて下さい．複数名の査読者による研究の発展性・重要性・根拠の確かさ・説明の明瞭さの評価をもとにプログラム委員会で議論し，採否を判断します．特に以下の点にご注意ください．・理論的な研究については，形式化の明瞭さと正しさが重要です．論文中に明　示してあれば証明等が未完成でも構いませんが，証明等について議論できる　程度の完成度は求められます．・実装技術の研究については，手法の妥当性や評価が重要です．論文中に明示　してあれば実装や実験が未完成でも構いませんが，上記の点を議論できる程　度の完成度は求められます．・ソフトウェアやツールの実現に関する研究については，その有用性やデザイ　ンチョイスが明瞭であることが重要です．論文中に明示してあれば実装が未　完成でも構いませんが，上記の点を議論できる程度の完成度は求められます．カテゴリ2 では，国際会議や国際学術論文誌等で発表済みまたは採録決定済みの，自身が著者の一人に含まれている研究論文の紹介を募集します．PPLとの関連性，プログラム全体のバランス，発表された媒体等をもとにプログラム委員会で議論し，採否を判断します．カテゴリ3 では，PPL に関連する内容（未発表・既発表いずれでも構いません）についてのポスター発表を募集します．萌芽的なアイデアの紹介やツールのデモンストレーションなども歓迎します．PPLとの関連性・プログラム全体のバランスをもとに，プログラム委員による議論によって採否を判断します．カテゴリ4 では，研究動向の紹介・分野間の相互理解・ツールのチュートリアルなど，PPL の聴衆にとって有益な学術知識の紹介を募集します．未発表・既発表の別を問いません．PPL との関連性，内容の重要性，発表者の経歴，プログラム全体のバランス等をもとにプログラム委員会で議論し，採否を判断します．カテゴリ1 の採択論文の中から，特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．さらに，カテゴリ1・2 の全発表のなかから最も聴衆の支持を集めたものに発表賞，カテゴリ3 の全発表のなかから最も聴衆の支持を集めたものにポスター賞を授与する予定です（いずれも一般の部・学生の部の 2種類，ただし「発表賞」は既受賞者を除く）． ** プログラム委員会 ** プログラム共同委員長　塚田武志（千葉大学）プログラム共同委員長　日高宗一郎（法政大学）荒堀喜貴　　　　（東京工業大学）池渕未来　　　　（京都大学）伊澤侑祐　　　　（東京都立大学）上田和紀　　　　（早稲田大学）鵜川始陽　　　　（東京大学）馬谷誠二　　　　（神奈川大学）紙名哲生　　　　（大分大学）亀山幸義　　　　（筑波大学） Jacques Garrigue 　（名古屋大学）木村大輔　　　　（東邦大学）内藏理史　　　　（早稲田大学）佐々木晃　　　　（法政大学）宋剛秀　　　　　（神戸大学）田邉裕大　　　　（東京工業大学）千代英一郎　　　（成蹊大学）寺内多智弘　　　（早稲田大学）中野圭介　　　　（東北大学）中丸智貴　　　　（東京大学）西田直樹　　　　（名古屋大学）西田雄気　　　　（東北大学）長谷川真人　　　（京都大学）平石拓　　　　　（京都橘大学）福原淳司　　　　（（株）デンソー）松下祐介　　　　（京都大学）八杉昌宏　　　　（九州工業大学） ** 組織委員会 ** 組織委員長　　　　　　　堀江倫大　（日本IBM）組織副委員長　　　　　　木村大輔　（東邦大学）財務担当　　　　　　　　田邉裕大　（東京工業大学）財務副担当　　　　　　　池渕未来　（京都大学）会場担当　　　　　　　　中丸智貴　（東京大学）会場副担当　　　　　　　松田直祐　（湘南工科大学）渉外担当　　　　　　　　叢悠悠　　（東京工業大学）プログラム共同委員長　　日高宗一郎（法政大学）プログラム共同委員長　　塚田武志　（千葉大学）前プログラム共同委員長　安部達也　（千葉工業大学）前プログラム共同委員長　川端英之　（広島市立大学） ** 問い合わせ先 ** ・ワークショップ全般について（メールの件名に [PPL2025] と付けていただけるでしょうか）　組織委員長：horie[at]jp.ibm.com ・発表/プログラムについて　プログラム共同委員長：ppl2025-pc-chairs[at]easychair.org ================================================ -- 法政大学情報科学部コンピュータ科学科日高宗一郎 hidaka[at]hosei.ac.jp

1 0

【発表募集・締切延長】第151回プログラミング研究発表会（PRO-2024-3）
by Sosuke MORIGUCHI 13 Sep '24

13 Sep '24

※重複してお受け取りの場合はご容赦ください．皆様東京工業大学の森口と申します．情報処理学会第151回プログラミング研究発表会（PRO-2024-3）の発表申込の締切を延長しました（9/13→9/20）ので，再度ご案内させていただきます．ご検討のほどよろしくお願いいたします． ==== 情報処理学会第151回プログラミング研究発表会発表募集 https://sigpro.ipsj.or.jp/pro2024-3/ 日時：2024年11月12日(火)〜11月13日(水) 会場：東京科学大学（9月まで東京工業大学）大岡山キャンパス　　　およびオンラインのハイブリッド開催を予定参加費：無料発表申込締切：2024年9月13日（金）→2024年9月20日（金）（延長しました）投稿論文原稿提出締切：2024年10月7日（月）発表予稿提出締切：2024年11月08日（金）プログラミング研究会（PRO）は， * プログラミング言語の設計，処理系の実装 * プログラミングの理論，基本概念 * プログラミング環境，支援システム * プログラミング方法論，パラダイム * これらを応用したシステムの開発事例 * その他，プログラミングに関する面白い話題を対象とした研究発表の場です．研究会と密接にリンクした論文誌を1998年度から毎年3〜4回のペースで発行しており，研究発表会での発表内容を論文誌に投稿することができます．発表申込時に投稿を希望し投稿締切までに原稿が提出されている論文が査読の対象となります．採否は研究発表会からおおむね 3週間ほどで迅速に決定されます．論文誌への投稿を希望しない発表も歓迎します． 1件あたりの発表時間は45分（発表25分，質疑20分）です．通常の発表に加え，「短い発表」も募集します．「短い発表」の発表時間は30分（発表20分・質疑10分）です．発表内容は通常の発表と同様ですが，特に，萌芽的なアイデアの提示，進行中の研究の途中報告，システム開発経験や興味深いプログラミング技法の紹介，開発したツールやソフトウェアの紹介などを「短い発表」として歓迎します．発表資料は数ページ程度の短いもので結構です．ただし，「短い発表」の論文誌への投稿はできません．英語論文の投稿も歓迎します．2015年度以降，英語論文が採録された場合，その論文の正本は英語論文誌JIPに掲載されます．また，和文論文を採録決定後に英語化し英語論文として掲載する試みを行っています．英語論文の投稿をご検討の方は以下のアナウンスをご覧ください． https://sigpro.ipsj.or.jp/sigtra4/ 「5．英文論文誌JIPとの連携」「6. 和文論文の採録後の英語化」多くの発表ならびに論文投稿をお待ちしております．担当者：森口草介（東京工業大学），緒方一則（日本IBM）問い合わせ先：chiguri(a)c.titech.ac.jp

1 0

数学基礎論サマースクール
by YOKOYAMA Keita 10 Sep '24

10 Sep '24

みなさま，東北大学の横山です．今年度の数学基礎論サマースクールにつきまして，以下の要領で開催したいと考えております．日時: 9月17日〜20日(4日間) 場所: 東北大学情報科学研究科(青葉山キャンパス) テーマ: 算術の証明論と構成的数学講師: 倉橋先生，根元先生，横山，他1-2名にお願いする予定ですご質問等ございましたら，世話人の横山 keita.yokoyama.c2[at]tohoku.ac.jp までお問い合わせください．より詳しいことが決まりましたら，またご案内させていただきます．どうぞよろしくお願いいたします．横山啓太 -- Keita Yokoyama Mathematical Institute, Tohoku University keita.yokoyama.c2(a)tohoku.ac.jp

1 2

【発表募集】第151回プログラミング研究発表会（PRO-2024-3）
by Sosuke MORIGUCHI 09 Sep '24

09 Sep '24

※重複してお受け取りの場合はご容赦ください．皆様東京工業大学の森口と申します．情報処理学会第151回プログラミング研究発表会（PRO-2024-3）の発表申込の締切（9/13）が近づいてまいりましたので，再度ご案内させていただきます．ご検討のほどよろしくお願いいたします． ==== 情報処理学会第151回プログラミング研究発表会発表募集 https://sigpro.ipsj.or.jp/pro2024-3/ 日時：2024年11月12日(火)〜11月13日(水) 会場：東京科学大学（9月まで東京工業大学）大岡山キャンパス　　　およびオンラインのハイブリッド開催を予定参加費：無料発表申込締切：2024年9月13日（金）投稿論文原稿提出締切：2024年10月7日（月）発表予稿提出締切：2024年11月08日（金）プログラミング研究会（PRO）は， * プログラミング言語の設計，処理系の実装 * プログラミングの理論，基本概念 * プログラミング環境，支援システム * プログラミング方法論，パラダイム * これらを応用したシステムの開発事例 * その他，プログラミングに関する面白い話題を対象とした研究発表の場です．研究会と密接にリンクした論文誌を1998年度から毎年3〜4回のペースで発行しており，研究発表会での発表内容を論文誌に投稿することができます．発表申込時に投稿を希望し投稿締切までに原稿が提出されている論文が査読の対象となります．採否は研究発表会からおおむね 3週間ほどで迅速に決定されます．論文誌への投稿を希望しない発表も歓迎します． 1件あたりの発表時間は45分（発表25分，質疑20分）です．通常の発表に加え，「短い発表」も募集します．「短い発表」の発表時間は30分（発表20分・質疑10分）です．発表内容は通常の発表と同様ですが，特に，萌芽的なアイデアの提示，進行中の研究の途中報告，システム開発経験や興味深いプログラミング技法の紹介，開発したツールやソフトウェアの紹介などを「短い発表」として歓迎します．発表資料は数ページ程度の短いもので結構です．ただし，「短い発表」の論文誌への投稿はできません．英語論文の投稿も歓迎します．2015年度以降，英語論文が採録された場合，その論文の正本は英語論文誌JIPに掲載されます．また，和文論文を採録決定後に英語化し英語論文として掲載する試みを行っています．英語論文の投稿をご検討の方は以下のアナウンスをご覧ください． https://sigpro.ipsj.or.jp/sigtra4/ 「5．英文論文誌JIPとの連携」「6. 和文論文の採録後の英語化」多くの発表ならびに論文投稿をお待ちしております．担当者：森口草介（東京工業大学），緒方一則（日本IBM）問い合わせ先：chiguri(a)c.titech.ac.jp

1 0

Giovanni Sambin教授講演 Sept. 10th Hybrid 三田ロジックミーティング
by Kentaro Ozeki 06 Sep '24

06 Sep '24

皆さま東京大学の小関と申します。 Giovanni Sambin 教授 (University of Padua) をお招きして、慶應義塾大学三田キャンパスにて下記の通りご講演いただきます。オンライン参加も可能です。ご興味をお持ちの方はぜひご参加ください。 ======== 以下告知文 ======== 三田ロジックミーティング Giovanni Sambin教授講演 Logic Seminar - Prof. Giovanni Sambin's Talk 2024年9月10日（火）September 10th (Tue.), 17:00-19:00 (JST) (ハイブリッド開催 Hybrid) ＊要事前登録・対面参加の方もお願いします。Pre-registration is required for both online and in-person participants. ◆講演者 / Speaker: Prof. Giovanni Sambin (University of Padua) ◆タイトル / Title: "From constructive topology to dynamics in foundations, and back" アブストラクトは以下をご覧ください。Abstract attached below. 場所 / Venue: オープンラボ（三田キャンパス東館4階） OpenLab (Mita Campus East Building, 4th Floor) キャンパスマップ 13番の建物: https://www.keio.ac.jp/ja/maps/mita.html Campus Map Building #13: https://www.keio.ac.jp/en/maps/mita.html Please pre-register here. / ここから事前登録をお願いします。オンライン参加の方には Zoomリンクをお送りします。 https://forms.gle/rnbLFoMV9RgsGB8p8 最新情報は次のページをご覧ください。See below for the updated information. https://abelard.flet.keio.ac.jp/2024/sambin_202409/ ＊URLは一両日中に開設されます。《PROGRAM》 ◆17:00-18:30 Speaker: Prof. Giovanni Sambin Title: "From constructive topology to dynamics in foundations, and back" ◆18:30-19:00 Discussion お問い合わせ先: logic(a)abelatd.flet.keio.ac.jp Organizers: Risako Ando, Koji Mineshima, Mitsuhiro Okada (Keio University), Kentaro Ozeki (University of Tokyo) ---------------------------------------------------------- アブストラクト / ABSTRACT "From constructive topology to dynamics in foundations, and back" We show that topology, understood as a mathematical discipline, is the basis of a dynamic vision of mathematics in which the main criterion is a genuine interaction with reality and not just the mere absence of contradictions. The distinction between real mathematics, expressed by pointfree topology, and ideal mathematics, expressed by the notions of ideal point and ideal space, allows the development of an abstract mathematics, such as that which began at the end of the 19th century with set theory, but which does not suffer from the abstrusities of the usual axiomatic set theory and, in particular, maintains the priority of the effective and computational aspects of mathematics. This could be the beginning of a new paradigm in mathematics in the sense of Thomas Kuhn, or rather the completion of the revolution initiated by Frege and Cantor, in which however mathematics is seen not as a given absolute truth, but rather as a cultural product constructed by humanity. ----------------------------------------------------------

1 0

【参加登録開始】PPLサマースクール2024「分離論理 Iris の世界」のご案内【9/9 @ 立命館大学&オンライン】
by Kazutaka Matsuda 28 Aug '24

28 Aug '24

皆様（複数お受取になった場合はご容赦ください），東北大学の松田と申します．先日案内しておりました，日本ソフトウェア科学会第41回大会 (https://jssst2024.wordpress.com/) 併設イベント PPLサマースクール2024「分離論理 Iris の世界」日時：2024年9月9日(月) 13:00〜16:25 場所：立命館大学大阪いばらきキャンパスおよびオンラインのハイブリッド開催講師：松下祐介（京都大学情報学研究科）の参加登録が始まっておりますので，再度ご案内さしあげます．参加登録方法について https://jssst2024.wordpress.com/participation/ をご参照下さい．上記に書かれております通り，今年は， (1) 立命館大学の学生 (2) (1)以外でPPLサマースクールのみに参加する学生 (3) (1)と(2)以外の方々で参加窓口が分かれております．興味のある方はどうぞご参加を検討いただけますと幸いです．特に会員・非会員問わず学生の参加費は無料となっておりますので，是非気軽に参加いただければと存じます． ========== http://ppl.jssst.or.jp/index.php?ss2024 # PPLサマースクール2024「分離論理 Iris の世界」日時：2024年9月9日(月) 13:00〜16:25 場所：立命館大学大阪いばらきキャンパスおよびオンラインのハイブリッド開催講師：松下祐介（京都大学情報学研究科） PPLサマースクール2024は対面を中心としたハイブリッド形式で開催いたします．大会自体は対面のみの開催であることにご注意ください． ## 概要プログラム検証における本質的な困難の一つが、メモリ上の可変オブジェクトに代表される、「可変状態」です。2001年に O'Hearn らが築いた「分離論理」は、論理式に所有権を持たせるというアイデアで、可変状態についてのスケーラブルな推論を実現しました。分離論理はプログラム検証における一大分野として非常に活発に研究されています。特に、並行計算への拡張「並行分離論理」は2016年に Gödel 賞を受賞しました。そうした中で特に注目されているのが、 2015年に Jung らが開発した高階並行分離論理フレームワーク「Iris」 https://iris-project.org/ です。Iris は多くの推論機構を包摂する、拡張性の高い汎用分離論理フレームワークであり、定理証明支援系 Coq 上の成熟したライブラリとして機械化されています。Rust の所有権型システムを検証した2018年 Jung らの「RustBelt」を筆頭に、ここ数年 Iris を用いる論文が PL系トップ国際会議に多数採択されており、2023年には Iris の功績に Church 賞が与えられました。この講義では、実際に Iris を使う研究に取り組む松下氏を講師としてお招きし、分離論理の初歩からはじめて、現代的な分離論理の基礎、Iris の発展的話題、Iris の Rust への応用といったトピックについて解説いただきます。 ## 講師紹介松下祐介（京都大学情報学研究科）現在京都大学大学院情報学研究科五十嵐・末永研究室特定研究員 (学振 PD)。2024年東京大学大学院情報理工学系研究科コンピュータ科学専攻博士課程修了 (指導教員: 小林直樹教授)、博士 (情報理工学)。2019年東京大学理学部情報科学科卒業。 Rust プログラムを「預言」の手法でステートレスな表現に帰着して自動検証する「RustHorn」(松下ら、ESOP '20・TOPLAS '21) が代表作。RustHorn 流帰着の正しさを分離論理 Iris で証明する、ドイツ MPI-SWS RustBelt/Iris チームとの共同研究「RustHornBelt」(松下ら、 PLDI '22) 、Iris の鍵となる高階幽霊状態という機能における later 様相の問題を解決する研究「Nola」(松下、博論 '24) など、分離論理 Iris を使う研究にも従事。 ## プログラム 13:00 - 13:05 オープニング 13:05 - 14:05 現代的な分離論理の基礎 14:05 - 14:25 休憩 14:25 - 15:25 Iris の発展的話題 15:25 - 15:45 休憩 15:45 - 16:45 Iris × Rust ### 現代的な分離論理の基礎 2001年に生まれた分離論理は、現代にいたるまでの20数年で急速に発展しています。この部では、分離論理の初歩からはじめて、Iris による高度な拡張にいたるまで、現代的な分離論理の基礎を解説します。 ### Iris の発展的話題この部では、Iris の発展的な話題について説明します。 Iris で鍵となる仕組みである「高階幽霊状態」、これを扱うための「later 様相」や「step-indexing」といった機能について説明します。これに関連して、講師の博士論文の成果となった研究「Nola」についても話します。また、Iris が Coq ライブラリとしてどのような設計になっているか、Iris を使ってどのように可変状態を扱う検証プロジェクトを Coq で機械化できるかについても説明します。 ### Iris × Rust Iris の重要な応用例の一つが、2015年に生まれたプログラミング言語「Rust」の所有権型についての検証です。2018年の Jung らによる「RustBelt」は、 Rust で鍵となる仕組みである「借用」を Iris でモデル化し、Rust のメモリ・スレッド安全性保証を検証しました。2022年の松下らによる「RustHornBelt」は、RustBelt を拡張し、RustHorn 流の帰着の正しさを一般に証明しました。この部では、こうした Iris の Rust への応用について、実際に RustHornBelt の研究に取り組んだ経験を踏まえて解説します。 ## 参加費一般会員：1000円一般非会員：2000円学生会員, 学生非会員：無料 ## 問い合わせ先 PPLサマースクール2024 幹事松田一孝（東北大学） E-mail: kztk(a)tohoku.ac.jp

1 0

← Newer
1
2
3
4
5
6
7
...
180
Older →

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml