Universal Algebraic Datatypes: Theory and Practice on Datatypes based on Higher-Order Rewriting

Research Project

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 2020)
Budget Amount *help	¥17,550,000 (Direct Cost: ¥13,500,000、Indirect Cost: ¥4,050,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) プログラミング」の理論の確立と実践を目的とする。真代数データ型は、「代数」をデータとプログラムの単位とすることで安全性を保証する。さらに代数の等式公理から、計算規則を自動導出することで、高速で柔軟な実行アルゴリズムを提供する。