Page 334 - 《软件学报》2021年第6期

1908 Journal of Software 软件学报 Vol.32, No.6, June 2021

式化证明工作中,我们不仅证明了分块矩阵运算的正确性,并将矩阵形式化中已证明的函数移植于分块矩阵形
式化库中.最后,我们建立了基于不同类型的分块矩阵基础库.目前,我们已经实现用函数式语言描述矩阵,在未
来的工作中,我们考虑定义一组重写优化规则并进行代码优化,将该矩阵运算以及分块矩阵运算函数转换为高
效率并行 C 代码,并验证该重写优化的等价性,从而构建一个深度学习代码优化系统,并完成深度学习矩阵运算
的形式化验证.
本次研究工作的代码地址:https://gitee.com/yingyingma/Matrix.

致谢 感谢石正璞对本次工作提出的问题和建议以及在编译方面的支持工作,感谢沈楠、邓昊对本文存在的语
病和问题的检查和纠正,感谢张正、崔敏以及讨论班的同学对本次研究工作的热心讨论和研究.

References:
[1] Almeida JB, Frade MJ, Pinto JS, Sousa SMD. An overview of formal methods tools and techniques. In: Proc. of the Rigorous
Software Development. London: Springer-Verlag, 2011. 15−44.
[2] Formalizing the safety of Java, the Java virtual machine, and Java card. ACM Computing Surveys (CSUR), 2001,33(4).
[3] Ma ZW, Chen G. Matrix formalization based on Coq record. Computer Science, 2019,46(7):139−145 (in Chinese with English
abstract). [doi: 10.11896/j.issn.1002-137X.2019.07.022]
[4] Hagedorn B, Lenfers J, Koehler T, Qin XY, Gorlatch S, Steuwer M. Achieving high-performance the functional way—A functional
pearl on expressing high-performance optimizations as rewrite strategies. In: Proc. of the ACM SIGPLAN Int’l Conf. on Functional
Programming (ICFP 2020). 2020. [doi: 10.1145/3408974]
[5] Bertot Y, Casteran P. Interactive theorem proving and program development. In: Proc. of the Coq’Art: The Calculus of Inductive
Constructions. Springer, 2004.
[6] Obua S. Proving bounds for real linear programs in Isabelle/HOL. In: Proc. of the Theorem Proving in Higher Order Logics. 2005.
227−244.
[7] Paşca I. Formal proofs for theoretical properties of Newton’s method. Mathematical Structures in Computer Science, 2011,21(4).
[doi: 10.1017/S0960129511000077]
[8] Paşca I. Formally verified conditions for regularity of interval matrices [Ph.D. Thesis]. Intelligent Computer Mathematics, 2010.
[9] Alama J. The rank-nullity theorem. Formalized Mathematics, 2007,15(3).
[10] Karol PK. Eigenvalues of a linear transformation. Formalized Mathematics, 2008,16(4):289−295. [doi: 10.2478/v10037-008-
0035-x]
[11] Solovay RM, Arthan RD, Harrison J. Some new results on decidability for elementary algebra and geometry. Annals of Pure and
Applied Logic, 2012,163(12). [doi: 10.1016/j.apal.2012.04.003]
[12] Shi ZP, Liu ZK, Guan Y, Ye SW, Zhang J, Wei HX, Luo GM. Formalization of function matrix theory in HOL. Journal of Applied
Mathematics, 2013,34(3):654−658 (in Chinese with English abstract). [doi: 10.1155/2014/201214]
[13] Kang XN, Shi ZP, Ye SW, Guan Y. Formalization of matrix transformation theory in HOL4. Computer Simulation, 2014,31(3):
289−294 (in Chinese with English abstract). [doi: 10.1080/19443994.2014.944221]
[14] Yang XM, Guan Y, Shi ZP, Wu AX, Zhang QY, Zhang J. Higher-Order logic formalization of function matrix and its calculus.
Computer Science, 2016,43(11):24−29 (in Chinese with English abstract). [doi: 10.11896/j.issn.1002-137X.2016.11.005]
[15] https://math-comp.github.io/mcb/
[16] Boldo S, Lelay C, Melquiond G. Coquelicot: A user-friendly library of real analysis for Coq. Mathematics in Computer ence, 2015,
9(1):41−62. [doi: 10.1007/s11786-014-0181-1]
附中文参考文献:
[3] 马振威,陈钢.基于 Coq 记录的矩阵形式化方法.计算机科学,2019,46(7):139−145. [doi: 10.11896/j.issn.1002-137X.2019.07. 022]
[12] 刘振科,施智平,关永,等.函数矩阵理论在 HOL4 中的形式化.小型微型计算机系统,2013,34(3):654−658. [doi: 10.1155/2014/
201214]