Dependent refinement types and predicate constraints for program verification
| Project/Area Number |
23K24826
|
|---|
| Project/Area Number (Other) |
22H03570 (2022-2023)
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Multi-year Fund (2024)
Single-year Grants (2022-2023) |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
寺内 多智弘 早稲田大学, 理工学術院, 教授 (70447150)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
海野 広志 東北大学, 電気通信研究所, 教授 (80569575)
|
|---|
| Project Period (FY) |
2022-04-01 – 2027-03-31
|
| Project Status |
Granted (Fiscal Year 2024)
|
| Budget Amount *help |
¥16,770,000 (Direct Cost: ¥12,900,000、Indirect Cost: ¥3,870,000)
Fiscal Year 2026: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000)
Fiscal Year 2025: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000)
Fiscal Year 2024: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000)
Fiscal Year 2023: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000)
Fiscal Year 2022: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
|
|---|
| Keywords | プログラム検証 / 依存篩型 / 述語制約 / 自動定理証明 / 不動点論理 / 型システム / 述語制約解消 / 代数的エフェクト |
|---|
| Outline of Research at the Start |
本研究の目標は、型理論と制約解消技術によるソフトウェアプログラムの正しさの検証である。特に、「依存篩型(dependent refinement types)」と「述語制約(predicate constraint)」を用いた手法の深化を目指す。
|
| Outline of Annual Research Achievements |
代数的エフェクトハンドラを含むプログラムのための依存篩型によるプログラム検証手法について研究を行った。具体的には、これまでの型推論と述語制約解消による手法を、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)に採録された。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究はおおむね順調に進展している。「研究実績の概要」で述べた通り、今年度は主に代数的エフェクトハンドラを含むプログラムのための依存篩型システムに関する研究を行い成果を得た。
また、述語制約解消と自動定理証明に関する研究としては、前年度に提案した双対性をうまく用いた解消解消・不動点論理のための自動定理手法について引き続き研究を行っており、こちらの研究もおおむね順調に進展している。
|
| Strategy for Future Research Activity |
引き続き述語制約および不動点論理に関する研究を行う。特に、前年度開発した、述語制約への帰着と不動点論理の双対性を用いた新たな不動点論理妥当性判定手法の応用および手法のさらなる深化を目指す。加えて、引き続き代数的エフェクトハンドラや多相再帰(polymorphic recursion)など型システムに関する研究を行う。
|
Report
(2 results)
Research Products
(25 results)
