Principles of Higher-Order Universal Algebraic Datatypes
Project/Area Number |
17K00092
|
Research Category |
Grant-in-Aid for Scientific Research (C)
|
Allocation Type | Multi-year Fund |
Section | 一般 |
Research Field |
Software
|
Research Institution | Gunma University |
Principal Investigator |
Hamana Makoto 群馬大学, 大学院理工学府, 准教授 (90334135)
|
Project Period (FY) |
2017-04-01 – 2021-03-31
|
Project Status |
Completed (Fiscal Year 2020)
|
Budget Amount *help |
¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2019: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2018: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2017: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
|
Keywords | 関数プログラミング / 書換え系 / 代数仕様 / プログラム理論 / 合流性 / ラムダ計算 / 停止性 / 関数プログラム / 型理論 / 自動証明 / ソフトウェア科学 / 項書き換え系 / 代数データ型 |
Outline of Final Research Achievements |
As information systems have become one of the important infrastructures, the assurance of dependable software has become an important social and research problem. The aim of this study is to propose a new principle of higher-order algebra-oriented programming as a basis of dependable software. For this purpose, I studied the theory of higher-order rewriting systems from various aspects and developed a Haskell-based analysis tool, SOL, Second-Order Laboratory. Using it, I have proved the decidability of various computational systems.
|
Academic Significance and Societal Importance of the Research Achievements |
高階代数系を基礎とするプログラミング言語のための有用な研究成果をあげた。特にSOLシステムを用いることにより、プログラミング言語論と関係する様々な体系が二階書換えの理論で取り扱えることがわかった。高次元書換え理論とも関連するため、今後も重要な発展に繋がると期待できる
|
Report
(5 results)
Research Products
(17 results)
-
-
-
-
[Journal Article] Confluence Competition 20182018
Author(s)
T. Aoto, M. Hamana, N. Hirokawa, A. Middeldorp J. Nagele, N. Nishida, K. Shintani, and Harald Zankl
-
Journal Title
Leibniz International Proceedings in Informatics (LIPIcs)
Volume: 108
DOI
NAID
Related Report
Peer Reviewed / Open Access / Int'l Joint Research
-
-
-
-
-
-
-
-
-
-
-
-
-