| 講演名 | 2023-01-11 例外を含む関数型言語の形式的記述と停止性証明のための制約付き依存対 濱口 毅(名大), 酒井 正彦(名大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本発表では例外処理を持つ関数型プログラムの停止性証明手法を提案する．まず先行評価に基づくプログラムの詳細な評価順序の形式的記述を与える．そして，項書換え系などの停止性証明で利用されている依存対法を応用するために，プログラムから生成される制約付き依存対を定義し，停止性証明法を与える．また，停止性証明の健全性と完全性の証明の概略を示す． |
| 抄録(英) | This paper proposes a termination-proof method for functional programs with exception handling. First, we give a small step semantics as a formal description to describe the precise eager-evaluation order for one of such languages. Based on the dependency pair method for termination proofs on term rewriting systems, we define constrained dependency pairs (CDP) and a termination proof method using CDP for the target programs. Then, we present outlined proofs of soundness and completeness of the method. |
| キーワード(和) | 関数型プログラム / 停止性 / 例外処理 / 制約付き依存対 |
| キーワード(英) | functional programs / termination / exception handling / constrained dependency pairs |
| 資料番号 | MSS2022-56,SS2022-41 |
| 発行日 | 2023-01-03 (MSS, SS) |
| 研究会情報 | |
| 研究会 | MSS / SS |
|---|---|
| 開催期間 | 2023/1/10(から2日開催) |
| 開催地（和） | 大阪市立生涯学習センター |
| 開催地（英） | |
| テーマ（和） | ソフトウェアサイエンス，システム数理と応用および一般 |
| テーマ（英） | |
| 委員長氏名（和） | 尾崎 敦夫(阪工大) / 岡野 浩三(信州大) |
| 委員長氏名（英） | Atsuo Ozaki(Osaka Inst. of Tech.) / Kozo Okano(Shinshu Univ.) |
| 副委員長氏名（和） | 山口 真悟(山口大) / 肥後 芳樹(阪大) |
| 副委員長氏名（英） | Shingo Yamaguchi(Yamaguchi Univ.) / Yoshiki Higo(Osaka Univ.) |
| 幹事氏名（和） | 小林 孝一(北大) / 劉 健全(NEC) / 小形 真平(信州大) / 林 晋平(東工大) |
| 幹事氏名（英） | Koichi Kobayashi(Hokkaido Univ.) / Jianquan Liui(NEC) / Shinpei Ogata(Shinshu Univ.) / Shinpei Hayashi(Tokyo Inst. of Tech.) |
| 幹事補佐氏名（和） | 白井 匡人(島根大) / ?本 真佑(阪大) |
| 幹事補佐氏名（英） | Masato Shirai(Shimane Univ.) / Shinsuke Matsumoto(Osaka Univ.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Mathematical Systems Science and its Applications / Technical Committee on Software Science |
|---|---|
| 本文の言語 | ENG-JTITLE |
| タイトル（和） | 例外を含む関数型言語の形式的記述と停止性証明のための制約付き依存対 |
| サブタイトル（和） | |
| タイトル（英） | A formal description of a functional language with exception handling, and constrained dependency pairs for the termination proofs |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 関数型プログラム / functional programs |
| キーワード(2)（和/英） | 停止性 / termination |
| キーワード(3)（和/英） | 例外処理 / exception handling |
| キーワード(4)（和/英） | 制約付き依存対 / constrained dependency pairs |
| 第 1 著者 氏名（和/英） | 濱口 毅 / Takeshi Hamaguchi |
| 第 1 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 第 2 著者 氏名（和/英） | 酒井 正彦 / Masahiko Sakai |
| 第 2 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 発表年月日 | 2023-01-11 |
| 資料番号 | MSS2022-56,SS2022-41 |
| 巻番号（vol） | vol.122 |
| 号番号（no） | MSS-329,SS-330 |
| ページ範囲 | pp.66-71(MSS), pp.66-71(SS), |
| ページ数 | 6 |
| 発行日 | 2023-01-03 (MSS, SS) |