Logic-ml August 2024

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

8 participants
9 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 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

【参加登録開始】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

日本ソフトウェア科学会第41回大会参加登録のご案内
by Tsuneyasu KOMIYA 26 Aug '24

26 Aug '24

皆様， # 重複してお受取になった場合はご容赦ください．電気通信大学の小宮と申します．槇原先生＠立命館大学のご依頼により，日本ソフトウェア科学会第41回大会の参加登録のご案内をさせていただきます．参加登録締切は，＊9月4日（水）＊までとなっております．皆様のご参加をお待ちしております． # PPL（プログラミング論研究会）以外のセッションの情報は，下記に記載の # 大会プログラムのページをご覧いただけたらと存じます． ---------------------------------------------------------------------- PPL関係者の皆様お世話になっております。日本ソフトウェア科学会第 41 回大会運営副委員長の槇原と申します。 9月9日（月）〜9月12日（木）にかけて開催される日本ソフトウェア科学会大会に関しまして、参加登録を開始いたしましたため、ご連絡を申し上げます。参加登録締切は、短くて恐縮ですが9月4日（水）まででございます。 PPL関係のセッションとして、以下が挙げられます。「項書き換え」「プログラミング言語の検証・圏論」「型」「論理・制約プログラミング」「言語設計・DSL」「組み込み向け言語」「プログラミング支援・ツール」「言語ランタイム・実装」イベント情報： ■PPLサマースクール 2024年9月9日(月) 13:00〜16:25 「分離論理 Iris の世界」講師：松下祐介氏（京都大学） ■2024年9月11日（水）基調講演1 松原仁（京都橘大学）「人間とAIの関係について将棋と囲碁の例から考える」 ■2024年9月12日（木）基調講演2 青木利晃（北陸先端科学技術大学院大学）「次世代車載基盤システムへの形式手法の実践」 ■2024年9月10日（火）大会企画講話高田広章教授（名古屋大学）「Software Defined Vehicle（SDV）− ソフトウェアは自動車をどのように変えるか？」大会ウェブサイト： https://jssst2024.wordpress.com/ 参加登録方法： https://jssst2024.wordpress.com/participation/ 大会プログラム： https://jssst2024.wordpress.com/program/ 皆様のご参加を心よりお待ちしております。 ================================ 以上になります。お忙しいところお手数をおかけいたしますが、何卒よろしくお願い申し上げます。槇原 ----------------------------------------------------------------------

1 0

RIMS共同研究（公開型）のご案内
by kota takeuchi 19 Aug '24

19 Aug '24

皆様下記のようにモデル理論の研究集会を行います。ご参加をお待ちしております。 --------------------------------------------------------------------------------- RIMS共同研究(公開型)「モデル理論における独立概念と次元の研究」日時：2023年12月4日(月)～2023年12月6日(水) 場所：京都大学数理解析研究所110室+オンライン(ZOOM) 代表者：竹内耕太（筑波大学）副代表：桔梗宏孝（神戸大学） Webページ： https://sites.google.com/gsuite.kobe-u.ac.jp/rimsmodeltheoryworkshop2023/ --------------------------------------------------------------------------------- 参加申し込みは上記webページからお願いします。 ※参加申し込みの情報は京都大学数理解析研究所および次年度世話人に提供されます．以上、よろしくお願いします。筑波大学竹内耕太

2 3

教員公募のご案内
by Satoru Kuroda 16 Aug '24

16 Aug '24

皆様，群馬県立女子大学の黒田です．現在，本学文学部文化情報学科では，情報系の教員公募をおこなっております．本学科は文学部内の学科ですが，情報科学，論理学の教員が複数在籍している分離融合型の学科で，数学や情報科学に関する講義を行なっていただくことを想定しております．適任の方がおられましたら，応募を検討いただくようお伝えいただければ幸甚に存じます．公募内容については以下の通りです．また詳細につきましては，大学のWebページ https://www.gpwu.ac.jp/inf/emp/emp_02/post_307/index.html#joho もしくはJREC-INでご確認ください．なお，授業コマ数が週５コマ程度とありますが，実際には授業を行わないコマも含みますので，実質の授業コマ数はこれより少なくなります．よろしくお願いいたします．１．募集職名・人員准教授または講師１名２．担当授業科目情報科学、情報工学関係の専門科目（情報数理、アルゴリズム論、オペレーティングシステム、情報システム論などから 1 つ以上。演習及び卒業研究指導含む）及び教養教育科目（情報処理）など週５コマ程度。さらに大学院修士課程の授業を担当していただくこともあります。３．応募資格（１）学歴博士の学位を持つ方（２）研究領域等情報科学または情報工学（情報科学あるいは情報工学における入門的指導を行える方が望ましい）（３）研究業績著書・論文が５点以上（修士、博士論文を含む）あり、かつ過去３年以内に研究業績のある方４．採用予定年月日 2025 年４月１日 -- Satoru Kuroda Gunma Prefectural Women's University

1 0

APLAS 2024 Call for Participation
by Mirai Ikebuchi 14 Aug '24

14 Aug '24

皆様，京都大学の池渕です．京都で開催される APLAS 2024 の Call for Participation をお送りします．皆様のご参加をお待ちしております．池渕 ------------- Call for Participation APLAS 2024 -- The 22nd Asian Symposium on Programming Languages and Systems October 22-24, 2024, Kyoto, Japan https://conf.researchr.org/home/aplas-2024/ Early Registration deadline: Sep 1 APLAS 2024 aims to bring together programming language researchers, practitioners and implementors *worldwide*, to present and discuss the latest results and exchange ideas in all areas of programming languages and systems. APLAS 2024 is co-located with the 22nd International Symposium on Automated Technology for Verification and Analysis (ATVA). Keynotes Albert Cohen (Google) Naoki Kobayashi (University of Tokyo: Joint with ATVA 2024) Sukyoung Ryu (KAIST, South Korea) Research Paper Sessions (18 papers) Student Research Competition and Poster Session APLAS-NIER post-conference workshop (Oct 25, 2024) Accepted Papers: A Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution Thi Thu Ha Doan, Peter Thiemann Building A Correct-By-Construction Type Checker for a Dependently Typed Core Language Bohdan Liesnikov, Jesper Cockx Comparing semantic frameworks of dependently-sorted algebraic theories Benedikt Ahrens, Peter Lefanu Lumsdaine, Paige Randall North Effective Search Space Pruning for Testing Deep Neural Networks Bala Rangaya, Eugene Sng, Minh-Thai Trinh Efficiently Adapting Stateless Model Checking for C11/C++11 to Mixed-Size Accesses Shigeyuki Sato, Taiyo Mizuhashi, Genki Kimura, Kenjiro Taura Explaining Explanations in Probabilistic Logic Programming German Vidal Extending the Quantitative Pattern-Matching Paradigm Sandra Alves, Delia Kesner, Miguel Ramos Generic Reasoning of the Locally Nameless Representation Yicheng Ni, Yuting Wang Hybrid Verification of Declarative Programs with Arithmetic Non-Fail Conditions Michael Hanus Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato Non-deterministic, probabilistic, and quantum effects through the lens of event structures Vitor Fernandes, Marc de Visme, Benoît Valiron OBRA: Oracle-based, relational, algorithmic type verification Lisa Vasilenko, Gilles Barthe, Niki Vazou On Computational Indistinguishability and Logical Relations Ugo Dal Lago, Zeinab Galal, Giulia Giusti Quantum Bisimilarity is a Congruence under Physically Admissible Schedulers Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, Gabriele Tedeschi Quantum Programming Without the Quantum Physics Jun Inoue Random-access lists, from EE to FP Pierre-Evariste Dagand, Titouan Quennet Relative Completeness of Incorrectness Separation Logic Yeonseok Lee, Koji Nakazawa Type-Based Verification of Connectivity Constraints in Lattice Surgery Ryo Wakizaka, Atsushi Igarashi, Yasunari Suzuki

1 0

CFP -- AWPL 2025
by 小野寛晰 13 Aug '24

13 Aug '24

===================================================== 7th Asian Workshop on Philosophical Logic 6-8 February, 2025 Department of Philosophy, Jadavpur University, Kolkata, India https://sites.google.com/view/awpl2025/ ===================================================== [CALL FOR PAPERS: EXTENSION OF DEADLINE] The 7th Asian Workshop on Philosophical Logic will be held on 6-8 February 2025 at the Department of Philosophy, Jadavpur University, Kolkata, India. Association for Logic in India (ALI [1]) will be a co-organizer for this workshop. The Asian Workshop on Philosophical Logic (AWPL [2]) is a series of events initiated by a group of Asian logicians. Its first instalment took place at JAIST in Japan in 2012. The workshop's primary goal is to promote awareness, understanding, and collaboration among researchers in philosophical logic and related fields. It emphasises the interaction between philosophical ideas and formal theories. AWPL 2025 will happen just after ICLA 2025 [3], which would be held at Indian Statistical Institute, Kolkata, India, during February 3-5, 2025. *Topics of interest include* (but are not restricted to): Algebraic logic; Chinese logic; Constructive logic; Decision Theory; Formal epistemology; Game Theory; Greek logic; Indian logic; Inductive logic; Logics of belief change; Logics of conditionals; Modal, temporal, epistemic and deontic logics; Nonmonotonic logics; Relevance and other non-classical logics; Philosophy of language; Philosophy of mathematics; Philosophy of Science; Proof Systems, Quantum logic; Vagueness; *as well as their applications in:* Artificial Intelligence, Cognitive Science; Computer Science; Law; Linguistics; Mathematics; Social Sciences. [1] https://logicindia.org/ [2] http://awpl.org/Workshops.html [3] https://logicindia.org/icla/icla2025 [IMPORTANT DATES] Submission deadline: 15 September, 2024 Notification of acceptance: 20 October, 2024 Workshop dates: 6-8 February, 2025 [SUBMISSION] All submissions should present original works that have not been previously published. Submissions should be written in English and follow the LNCS template [4]. Please prepare your submission as a PDF file with a maximum of 12 pages, including the reference list, appendixes, acknowledgements, etc. Submissions should be sent electronically via EasyChair [5] by the corresponding author within the specified deadline. It is expected that at least one of the authors will attend the workshop and present the accepted work. After the workshop, selected submissions will be invited to revise and resubmit for the post-conference proceedings, which will be published in the "Logic in Asia" [6] series. [4] https://www.springer.com/gp/computer-science/lncs/conference-proceedings-gu… [5] https://easychair.org/conferences/?conf=awpl2025 [6] http://www.springer.com/series/13080?detailsPage=titles [INVITED SPEAKERS] Bahareh Afshari (University of Gothenburg) Andreas Herzig (IRIT Toulouse) Fenrong Liu (Tsinghua University) Katsuhiko Sano (Hokkaido University) We will also have a distinguished lecture by: Johan van Benthem (Amsterdam, Stanford and Tsinghua) [STEERING COMMITTEE] Phan Minh Dung (Asian Institute of Technology, Bangkok) Hu Liu (Sun Yat-sen University, Guangzhou) Beishui Liao (Zhejiang University, Hangzhou) Fenrong Liu (Tsinghua University, Beijing) Hiroakira Ono (Japan Advanced Institute of Science and Technology, Ishikawa) R. Ramanujam (Azim Premji University, Bengaluru) Hsing-chien Tsai (National Chung Cheng University, Chiayi) [PROGRAM COMMITTEE] Rupa Bandyopadhyay (Jadavpur University) Mihir Chakraborty (Jadavpur University) Amita Chatterjee (Jadavpur University) Madhumita Chattopadhyay (Jadavpur University) Sujata Ghosh (Indian Statistical Institute) (Co-Chair) Purbita Jana (Madras School of Economics) Kohei Kishida (University of Illinois, Urbana-Champaign) Serafina Lapenta (University of Salerno) Dazhu Li (University of Chinese Academy of Sciences) Yanjun Li (Nankai University) Fei Liang (Shandong University) Abhishek Anant Nowbagh (Jadavpur University) (Co-Chair) Hitoshi Omori (Tohoku University) R.Ramanujam (Azim Premji University) Abhisekh Sankaran (Tata Consultancy Services Research) Manidipa Sanyal (University of Calcutta) Chenwei Shi (Tsinghua University) Sonja Smets (University of Amsterdam) Shawn Standefer (National Taiwan University) Sourav Tarafder (St. Xavier's College) Yanjing Wang (Peking University) Yì Nicholas Wáng (Sun Yat-sen University) Tomoyuki Yamada (Hokkaido University) Fan Yang (Utrecht University) [LOCAL ORGANIZING COMMITTEE] Gopinath Mondal (Jadavpur University, Kolkata) Samar Kumar Mondal (Jadavpur University, Kolkata) Tamoghna Sarkar (Jadavpur University, Kolkata) Mainak Pal (Jadavpur University, Kolkata) Sunirmal Das (Jadavpur University, Kolkata) [CONTACT] awpl2025ju(a)gmail.com

1 0

【学生無料】PPLサマースクール2024「分離論理 Iris の世界」のご案内【9/9 @ 立命館大学&オンライン】
by Kazutaka Matsuda 06 Aug '24

06 Aug '24

皆様（複数お受取になった場合はご容赦ください），東北大学の松田と申します．来たる9月9日に開催される，日本ソフトウェア科学会第41回大会 (https://jssst2024.wordpress.com/) 併設イベント， PPLサマースクール2024「分離論理 Iris の世界」についてご案内いたします．参加申し込みサイトはまだ準備中ですが近日中に下記リンク先にて公開予定です． https://jssst2024.wordpress.com/participation/ 興味ある方は是非カレンダーに予定を入れておいていただけると幸いです．学生は無料かつオンラインでも参加できますので是非参加を検討いただけばと存じます．（PPLサマースクールのみに参加する学生は参加申し込み窓口が異なる予定です．ご注意ください） ========== 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

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml August 2024