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: ¥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システムを用いることにより、プログラミング言語論と関係する様々な体系が二階書換えの理論で取り扱えることがわかった。高次元書換え理論とも関連するため、今後も重要な発展に繋がると期待できる

Research Products

• [Journal Article] Polymorphic computation systems: Theory and practice of confluence with call-by-value (2020)
  • Author(s): Makoto Hamana, Tatsuya Abe, Kentaro Kikuchi
  • Journal Title: Science of Computer Programming Volume: 187 Pages: 102322-102322
  • DOI: 10.1016/j.scico.2019.102322
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Journal Article] How to prove decidablity of equational theories with second-order computation analyser SOL (2019)
  • Author(s): M.Hamana
  • Journal Title: Journal of Functional Programming Volume: 29
  • DOI: 10.1017/s0956796819000157
  • Peer Reviewed
• [Journal Article] Polymorphic Rewrite Rules: Confluence, Type Inference, and Instance Validation (2018)
  • Author(s): M. Hamana
  • Journal Title: Lecture Notes in Computer Science Volume: 10818 Pages: 99-115
  • DOI: 10.1007/978-3-319-90686-7_7
  • ISBN: 9783319906850, 9783319906867
  • Peer Reviewed
• [Journal Article] Confluence Competition 2018 (2018)
  • 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: 10.4230/LIPIcs.FSCD.2018.32
  • NAID: 120006705615
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Journal Article] The Algebra of Recursive Graph Transformation Language UnCAL: Complete Axiomatisation and Iteration Categorical Semantics (2018)
  • Author(s): M. Hamana, K. Matsuda and K. Asada
  • Journal Title: Mathematical Structures in Computer Science Volume: 28 Issue: 2 Pages: 287-337
  • DOI: 10.1017/s096012951600027x
  • Peer Reviewed / Open Access
• [Journal Article] How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation (2017)
  • Author(s): M. Hamana
  • Journal Title: Proceedings of the ACM on Programming Languages Volume: Volume 1 Issue ICFP Issue: ICFP Pages: 1-5
  • DOI: 10.1145/3110266
  • Peer Reviewed / Open Access
• [Presentation] 高階パターン単一化のUnboundライブラリを用いたHaskellによる実装 (2021)
  • Author(s): 藤岡 亮, 浜名 誠
  • Organizer: 第23回プログラミングおよびプログラミング言語ワークショップ(PPL 2021)
• [Presentation] Polymorphic Rewrite Rules: Confluence, Type Inference, and Instance Validation (2018)
  • Author(s): M. Hamana
  • Organizer: International Symposium on Functional and Logic Programming 2018
  • Int'l Joint Research
• [Presentation] 関数プログラム・計算系の分割停止性検証: 外山-Klop-Barendregt の定理の高階化 (2018)
  • Author(s): 浜名誠
  • Organizer: 日本ソフトウェア科学会 第35回 高橋奨励賞
• [Presentation] The Algebra of Recursive Graph Transformation Language UnCAL: Complete Axiomatisation and Iteration Categorical Semantics (2018)
  • Author(s): M. Hamana
  • Organizer: Shonan Meeting - Diagrammatic Methods for Linear and Nonlinear Systems
  • Int'l Joint Research / Invited
• [Presentation] How to Prove Your Calculus is Decidable: Practical Applications of Second-order Algebraic Theories and Computation (2017)
  • Author(s): M. Hamana
  • Organizer: International Conference on Functional Programming
  • Int'l Joint Research
• [Presentation] A Functional Implementation of Function-as-Constructor Higher-Order Unification (2017)
  • Author(s): M. Hamana
  • Organizer: International Workshop on Unification (UNIF'17)
  • Int'l Joint Research
• [Presentation] SOL: Second-Order Laboratory (2017)
  • Author(s): Makoto Hamana, Tatsuya Abe, Yuito Murase, and Kazuhiko Sakaguchi.
  • Organizer: International Confluence Competition 2017
  • Int'l Joint Research
• [Presentation] SOL: A Tool for Proving Decidability of Equational Theories (2017)
  • Author(s): M. Hamana
  • Organizer: Shonan meeting on REVERSE EXECUTION IN TESTING - IMPROVING SECURITY AND RELIABILITY
  • Int'l Joint Research
• [Remarks] ホームページ
  • URL: http://www.cs.gunma-u.ac.jp/hamana/
• [Remarks] SOLシステムWebインターフェース
  • URL: http://www.sofsci.cs.gunma-u.ac.jp/solweb/
• [Remarks] Makoto Hamana home page
  • URL: http://www.cs.gunma-u.ac.jp/hamana/