典型文献
基于Coq的矩阵代码生成技术
文献摘要：
矩阵程序在智能系统中扮演着越来越重要的角色.随着矩阵应用的复杂性日益增加,生成正确矩阵代码的难度也在不断变大.并行硬件能够极大地提高矩阵运算的速度,然而,使用并行硬件进行编程以实现并行运算,需要编程人员在程序中描述功能以及如何利用硬件资源来交付结果.这些程序通常是命令式语言,难以推理并且重构,以尝试不同的并行化策略.在Coq中实现了由高级矩阵算子到C代码的矩阵表达式代码生成技术,其能够将带有执行策略的函数式矩阵代码转换为高效低级命令式代码.未来,将把矩阵的形式化同矩阵代码自动生成融合在一起,对矩阵代码转换的过程进行形式化验证,以保障生成的矩阵代码的可靠性,为实现基于矩阵形式化方法的高可靠性深度学习编译器的研制打下基础.
文献关键词：
定理证明;矩阵代码生成;形式化工程数学;高阶定理证明;Coq
中图分类号：
作者姓名：
麻莹莹;陈钢
作者机构：
南京航空航天大学 计算机科学与技术学院, 江苏 南京 211106
文献出处：
引用格式：
[1]麻莹莹;陈钢-.基于Coq的矩阵代码生成技术)[J].软件学报,2022(06):2224-2245
A类：
Coq,矩阵代码生成,形式化工程数学,高阶定理证明
B类：
生成技术,智能系统,矩阵应用,极大地提高,矩阵运算,并行运算,编程人员,硬件资源,交付,命令式,并行化,执行策略,代码转换,低级,代码自动生成,合在一起,形式化验证,矩阵形式,形式化方法,高可靠性,编译器,打下基础
AB值：
0.274418
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
