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's academic papers published 2 good results. Academic Papers Logical Methods in Computer Science This means that the new method of proof will be adopted. In this paper, we prove the stopping property of Call-by-Push-Value calculation system by using the theory of algebra, algebra and algebra. This is the first time that a person's speech has been used. The paper is about the convergence of Haskell's speech. Glasgow Haskell Compiler (GHC) is an optimization tool for Haskell Compilers. The GHC is the result of this study.

项目成果

高階パターン単一化の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(フランス)

因里亚（法国）