| 研究課題/領域番号 |
20H04164
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 群馬大学 |
|---|
研究代表者 |
浜名 誠 群馬大学, 情報学部, 准教授 (90334135)
|
|---|
| 研究分担者 |
室屋 晃子 京都大学, 数理解析研究所, 助教 (00827454)
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
今井 敬吾 岐阜大学, 工学部, 助教 (70456630)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2024-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
17,550千円 (直接経費: 13,500千円、間接経費: 4,050千円)
2023年度: 4,030千円 (直接経費: 3,100千円、間接経費: 930千円)
2022年度: 4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2021年度: 4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2020年度: 5,070千円 (直接経費: 3,900千円、間接経費: 1,170千円)
|
|---|
| キーワード | ソフトウェア科学 / 書換え系 / 代数仕様 / プログラム理論 / 関数プログラミング / 関数プログラム / 合流性 / 停止性 / Haskell / ラムダ計算 / 書替え系 |
|---|
| 研究開始時の研究の概要 |
情報システムが重要な社会基盤の一つとなるにつれ、ソフトウェアの安全性保証が大きな課題となっている。本研究は信頼性のあるソフトウェアの基盤技術としての「真代数データ型(Universal Algebraic Datatypes) プログラミング」の理論の確立と実践を目的とする。真代数データ型は、「代数」をデータとプログラムの単位とすることで安全性を保証する。さらに代数の等式公理から、計算規則を自動導出することで、高速で柔軟な実行アルゴリズムを提供する。
|
| 研究実績の概要 |
本年度は、書換え理論を高階多相型へ拡張し、停止性と合流性検証手法と、書換え規則の正当性検証手法を研究した。これにより、関数型プログラミング言語Haskellの書換え規則の正しさを自動的に検証する基礎理論が構築できた。
この結果をInternational Conference on Functional Programming (ICFP)併設のHaskellシンポジウム、および東京大学で開催された第40回日本ソフトウェア科学会大会で発表し、日本ソフトウェア科学会大会優秀発表賞を受賞した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
関数型プログラミング言語Haskellの書換え規則自動検証という未知の問題へ、二階書換え系の理論を拡張することができた。
|
| 今後の研究の推進方策 |
検証ツールの開発を進め、GHCにおけるCore書換え規則をより効果的に扱えるように実装を進める。
|
