| 研究課題/領域番号 |
23K24826
|
|---|
| 補助金の研究課題番号 |
22H03570 (2022-2023)
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 基金 (2024)
補助金 (2022-2023) |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 早稲田大学 |
|---|
研究代表者 |
寺内 多智弘 早稲田大学, 理工学術院, 教授 (70447150)
|
|---|
| 研究分担者 |
海野 広志 東北大学, 電気通信研究所, 教授 (80569575)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2027-03-31
|
| 研究課題ステータス |
交付 (2024年度)
|
| 配分額 *注記 |
16,770千円 (直接経費: 12,900千円、間接経費: 3,870千円)
2026年度: 3,380千円 (直接経費: 2,600千円、間接経費: 780千円)
2025年度: 3,120千円 (直接経費: 2,400千円、間接経費: 720千円)
2024年度: 3,380千円 (直接経費: 2,600千円、間接経費: 780千円)
2023年度: 3,120千円 (直接経費: 2,400千円、間接経費: 720千円)
2022年度: 3,770千円 (直接経費: 2,900千円、間接経費: 870千円)
|
|---|
| キーワード | プログラム検証 / 依存篩型 / 述語制約 / 自動定理証明 / 不動点論理 / 型システム / 述語制約解消 / 代数的エフェクト |
|---|
| 研究開始時の研究の概要 |
本研究の目標は、型理論と制約解消技術によるソフトウェアプログラムの正しさの検証である。特に、「依存篩型(dependent refinement types)」と「述語制約(predicate constraint)」を用いた手法の深化を目指す。
|
| 研究実績の概要 |
代数的エフェクトハンドラを含むプログラムのための依存篩型によるプログラム検証手法について研究を行った。具体的には、これまでの型推論と述語制約解消による手法を、Answer Type Modificationという限定継続等コントロールエフェクトのための型システムの概念とうまく組み合わせることにより、世界初の代数的エフェクトハンドラの動作を正確に解析することのできる依存篩型システムを開発した。この研究の成果をまとめた論文はプログラミング言語分野の最高峰の国際会議であるACM Symposium on Principles of Programming Languages(POPL)に採録された。
加えて、制約解消による文字列抽出のための正規表現の生成・修正に関する研究と、後方参照により拡張された正規表現の表現力に関する研究を行った。前者の研究の成果をまとめた論文はプログラミング言語分野の最高峰の国際会議であるACM Symposium on Programming Language Design and Implementation(PLDI)に採録された。後者の研究は理論計算機科学分野の難関国際会議であるInternational Symposium on Mathematical Foundations of Computer Science(MFCS)に採録された。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究はおおむね順調に進展している。「研究実績の概要」で述べた通り、今年度は主に代数的エフェクトハンドラを含むプログラムのための依存篩型システムに関する研究を行い成果を得た。
また、述語制約解消と自動定理証明に関する研究としては、前年度に提案した双対性をうまく用いた解消解消・不動点論理のための自動定理手法について引き続き研究を行っており、こちらの研究もおおむね順調に進展している。
|
| 今後の研究の推進方策 |
引き続き述語制約および不動点論理に関する研究を行う。特に、前年度開発した、述語制約への帰着と不動点論理の双対性を用いた新たな不動点論理妥当性判定手法の応用および手法のさらなる深化を目指す。加えて、引き続き代数的エフェクトハンドラや多相再帰(polymorphic recursion)など型システムに関する研究を行う。
|
