| 研究課題/領域番号 |
20H04164
|
|---|
| 研究機関 | 群馬大学 |
|---|
研究代表者 |
浜名 誠 群馬大学, 大学院理工学府, 准教授 (90334135)
|
|---|
| 研究分担者 |
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2024-03-31
|
| キーワード | 書換え系 / 関数プログラム / 合流性 / 停止性 / Haskell / ラムダ計算 |
|---|
| 研究実績の概要 |
本年度は学術論文誌論文2本出版の良好な成果を得た。
学術論文誌Logical Methods in Computer Science誌で発表した論文では、二階書換えの停止性に関する新しいモジュラーな証明法を確立した。これは意味ラベリング手法を拡張した新規な証明方法によるものである。さらに応用として、代数的効果、エフェクトハンドラ、 エフェクト理論を持つCall-by-Push-Value計算系の停止性を証明した。これは現実の関数型言語への有用な応用である。
論文誌コンピュータソフトウェア誌で発表した論文は、関数型言語Haskellのための合流性検証ツールを提案したものである。Glasgow Haskell Compiler (GHC)では、プログラマが Haskellプログラムを最適化するために書換え規則を使用することができる。これまで、GHCはユーザが定義した書換え規則の合流をチェックする方法がなかったが、本研究成果でこれを検証することができる。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
現実の関数型プログラミング言語Haskellへ、二階書換え系の合流性検証手法を拡張し、実装を与えることに成功した。
|
| 今後の研究の推進方策 |
二階書換えの基礎理論の拡充を進め、さらに関数型言語への有効な書換え手法の応用も進める。
|
