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

通用代数数据类型：基于高阶重写的数据类型理论与实践

• 批准号: 20H04164
• 负责人: 浜名 誠
• 金额: $ 11.23万
• 依托单位: Gunma University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2020
• 资助国家: 日本
• 起止时间: 2020-04-01 至 2024-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-20H04164/
• 关键词: ソフトウェア科学; 書換え系; 代数仕様; プログラム理論; 関数プログラミング; 書替え系; 関数プログラム; 合流性; 停止性; Haskell; ラムダ計算

本年度は学術論文誌論文2本出版の良好な成果を得た。学術論文誌Logical Methods in Computer Science誌で発表した論文では、二階書換えの停止性に関する新しいモジュラーな証明法を確立した。これは意味ラベリング手法を拡張した新規な証明方法によるものである。さらに応用として、代数的効果、エフェクトハンドラ、 エフェクト理論を持つCall-by-Push-Value計算系の停止性を証明した。これは現実の関数型言語への有用な応用である。論文誌コンピュータソフトウェア誌で発表した論文は、関数型言語Haskellのための合流性検証ツールを提案したものである。Glasgow Haskell Compiler (GHC)では、プログラマが Haskellプログラムを最適化するために書換え規則を使用することができる。これまで、GHCはユーザが定義した書換え規則の合流をチェックする方法がなかったが、本研究成果でこれを検証することができる。

This year, two academic articles and magazines have been published with "good results". The academic journal, Logical Methods in Computer Science, and other academic journals are listed in the following tables: the text, the second, the termination, the new information, the clear law and the establishment of the law. It means to know how to use new rules and regulations and to know how to do it. The results of algebra, the theory of physics, the theory of physics, the theory of algebra, the theory of physics, the theory of physics, I don't know how to use a few words. This is a list of articles, numerical expressions, Haskell, confluence, proposals, proposals, and so on. The Glasgow Haskell Compiler (GHC) protocol, the Haskell protocol, and the most efficient rules are used in the following rules. In this study, the results of this study show that the rules for the definition of health rules are not valid. The results of this study are not valid.

项目成果

高階パターン単一化のUnboundライブラリを用いたHaskellによる実装

使用 Unbound 库在 Haskell 中实现高阶模式统一

• 发表时间: 2021
• 作者: 藤岡 亮;浜名誠
• 通讯作者: 浜名誠

ホームページ

主页

The System SOL version 2020

系统 SOL 2020 版

• 发表时间: 2020
• 期刊: Proceedings of the 9th International Workshop on Confluence (IWC 2020)
• 作者: Makoto Hamana;Kentaro Kikuchi;Date Yao Faustin Dieudonne;Kazuki Fuju
• 通讯作者: Kazuki Fuju

A Functional Abstraction of Typed Invocation Contexts

类型化调用上下文的功能抽象

• DOI: 10.46298/lmcs-18
• 发表时间: 2022
• 期刊: Logical Methods in Computer Science
• 影响因子: 0.6
• 作者: Cong Youyou;Ishio Chiaki;Honda Kaho;Asai Kenichi
• 通讯作者: Asai Kenichi

Inria(フランス)

因里亚（法国）