2023 Fiscal Year Annual Research Report
Dependent refinement types and predicate constraints for program verification
| Project/Area Number |
22H03570
|
|---|
| Allocation Type | Single-year Grants |
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
寺内 多智弘 早稲田大学, 理工学術院, 教授 (70447150)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| Project Period (FY) |
2022-04-01 – 2027-03-31
|
| Keywords | プログラム検証 / 不動点論理 / 型システム / 自動定理証明 / 述語制約解消 / 代数的エフェクト |
|---|
| 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)など型システムに関する研究を行う。
|
Research Products
(15 results)
