Towards parallel programming environment with certified correctness and complexity

迈向具有经过认证的正确性和复杂性的并行编程环境

• 批准号: 15K15974
• 负责人: Emoto Kento
• 金额: $ 2.83万
• 依托单位: Kyushu Institute of Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2015
• 资助国家: 日本
• 起止时间: 2015-04-01 至 2019-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-15K15974/
• 关键词: 定理証明支援系; 並列プログラミング; 計算量; 不等式; 並列; 並列スケルトン; グラフ; 機械証明

项目成果

頂点部分集合変数を備えた大規模グラフ計算用領域特化言語

使用顶点子集变量进行大规模图计算的领域特定语言

• 发表时间: 2017
• 作者: 定平 典久;江本 健斗
• 通讯作者: 江本 健斗

Coqを用いた高度なプログラム運算定理の検証に向けて

使用 Coq 验证高级程序运算定理

• 发表时间: 2019
• 作者: 村田 康佑 ;江本 健斗
• 通讯作者: 江本 健斗

A DSL for graph parallel programming with vertex subsets

用于使用顶点子集进行图并行编程的 DSL

• DOI: 10.1007/s11227-019-02821-w
• 发表时间: 2019
• 期刊: The Journal of Supercomputing
• 作者: Kento Emoto;Fumihisa Sadahira
• 通讯作者: Fumihisa Sadahira

Coqにおける可読性の高い形式的証明に向けて

在 Coq 中实现高度可读的形式证明

• 发表时间: 2018
• 作者: 村田 康佑;江本 健斗
• 通讯作者: 江本 健斗

Coqにおける検証されたプログラム運算の拡張

在 Coq 中扩展经过验证的程序操作

• 发表时间: 2018
• 作者: 村田 康佑 ;江本 健斗
• 通讯作者: 江本 健斗