Universal Algebraic Datatypes: Theory and Practice on Datatypes based on Higher-Order Rewriting
| Project/Area Number |
20H04164
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
浜名 誠 群馬大学, 情報学部, 准教授 (90334135)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
室屋 晃子 京都大学, 数理解析研究所, 助教 (00827454)
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
今井 敬吾 岐阜大学, 工学部, 助教 (70456630)
|
|---|
| Project Period (FY) |
2020-04-01 – 2024-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥17,550,000 (Direct Cost: ¥13,500,000、Indirect Cost: ¥4,050,000)
Fiscal Year 2023: ¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000)
Fiscal Year 2022: ¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2021: ¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2020: ¥5,070,000 (Direct Cost: ¥3,900,000、Indirect Cost: ¥1,170,000)
|
|---|
| Keywords | ソフトウェア科学 / 書換え系 / 代数仕様 / プログラム理論 / 関数プログラミング / 書替え系 / 関数プログラム / 合流性 / 停止性 / Haskell / ラムダ計算 |
|---|
| Outline of Research at the Start |
情報システムが重要な社会基盤の一つとなるにつれ、ソフトウェアの安全性保証が大きな課題となっている。本研究は信頼性のあるソフトウェアの基盤技術としての「真代数データ型(Universal Algebraic Datatypes) プログラミング」の理論の確立と実践を目的とする。真代数データ型は、「代数」をデータとプログラムの単位とすることで安全性を保証する。さらに代数の等式公理から、計算規則を自動導出することで、高速で柔軟な実行アルゴリズムを提供する。
|
| Outline of Annual Research Achievements |
本年度は学術論文誌論文2本出版の良好な成果を得た。
学術論文誌Logical Methods in Computer Science誌で発表した論文では、二階書換えの停止性に関する新しいモジュラーな証明法を確立した。これは意味ラベリング手法を拡張した新規な証明方法によるものである。さらに応用として、代数的効果、エフェクトハンドラ、 エフェクト理論を持つCall-by-Push-Value計算系の停止性を証明した。これは現実の関数型言語への有用な応用である。
論文誌コンピュータソフトウェア誌で発表した論文は、関数型言語Haskellのための合流性検証ツールを提案したものである。Glasgow Haskell Compiler (GHC)では、プログラマが Haskellプログラムを最適化するために書換え規則を使用することができる。これまで、GHCはユーザが定義した書換え規則の合流をチェックする方法がなかったが、本研究成果でこれを検証することができる。
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
現実の関数型プログラミング言語Haskellへ、二階書換え系の合流性検証手法を拡張し、実装を与えることに成功した。
|
| Strategy for Future Research Activity |
二階書換えの基礎理論の拡充を進め、さらに関数型言語への有効な書換え手法の応用も進める。
|
Report
(2 results)
Research Products
(16 results)
