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): 菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
• Project Period (FY): 2020-04-01 – 2024-03-31
• Project Status: Granted (Fiscal Year 2021)
• Budget Amount: ¥17,550,000 (Direct Cost: ¥13,500,000、Indirect Cost: ¥4,050,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: ソフトウェア科学 / 書換え系 / 代数仕様 / プログラム理論 / 関数プログラミング

Outline of Research at the Start

情報システムが重要な社会基盤の一つとなるにつれ、ソフトウェアの安全性保証が大きな課題となっている。本研究は信頼性のあるソフトウェアの基盤技術としての「真代数データ型(Universal Algebraic Datatypes) プログラミング」の理論の確立と実践を目的とする。真代数データ型は、「代数」をデータとプログラムの単位とすることで安全性を保証する。さらに代数の等式公理から、計算規則を自動導出することで、高速で柔軟な実行アルゴリズムを提供する。