基于Coq的矩阵代码生成技术

来源：软件学报杂志2022年第6期北京时间：

作者：麻莹莹，陈钢

单位：麻莹莹，南京航空航天大学 计算机科学与技术学院, 江苏 南京 21110611,陈钢，南京航空航天大学 计算机科学与技术学院, 江苏 南京 21110602

摘要：矩阵程序在智能系统中扮演着越来越重要的角色.随着矩阵应用的复杂性日益增加,生成正确矩阵代码的难度也在不断变大.并行硬件能够极大地提高矩阵运算的速度,然而,使用并行硬件进行编程以实现并行运算,需要编程人员在程序中描述功能以及如何利用硬件资源来交付结果.这些程序通常是命令式语言,难以推理并且重构,以尝试不同的并行化策略.在Coq中实现了由高级矩阵算子到C代码的矩阵表达式代码生成技术,其能够将带有执行策略的函数式矩阵代码转换为高效低级命令式代码.未来,将把矩阵的形式化同矩阵代码自动生成融合在一起,对矩阵代码转换的过程进行形式化验证,以保障生成的矩阵代码的可靠性,为实现基于矩阵形式化方法的高可靠性深度学习编译器的研制打下基础.

关键词：定理证明;矩阵代码生成;形式化工程数学;高阶定理证明;Coq