| 研究課題/領域番号 |
20H04164
|
|---|
| 研究機関 | 群馬大学 |
|---|
研究代表者 |
浜名 誠 群馬大学, 情報学部, 准教授 (90334135)
|
|---|
| 研究分担者 |
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
今井 敬吾 岐阜大学, 工学部, 助教 (70456630)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2024-03-31
|
| キーワード | 書換え系 / 関数プログラム / 合流性 / 停止性 / Haskell / ラムダ計算 |
|---|
| 研究実績の概要 |
本年度は、書換え理論を高階多相型へ拡張し、停止性と合流性検証手法と、書換え規則の正当性検証手法を研究した。これにより、関数型プログラミング言語Haskellの書換え規則の正しさを自動的に検証する基礎理論が構築できた。
この結果をInternational Conference on Functional Programming (ICFP)併設のHaskellシンポジウム、および東京大学で開催された第40回日本ソフトウェア科学会大会で発表し、日本ソフトウェア科学会大会優秀発表賞を受賞した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
関数型プログラミング言語Haskellの書換え規則自動検証という未知の問題へ、二階書換え系の理論を拡張することができた。
|
| 今後の研究の推進方策 |
検証ツールの開発を進め、GHCにおけるCore書換え規則をより効果的に扱えるように実装を進める。
|
