函数矩阵及其微积分的高阶逻辑形式化 (Higher-order Logic Formalization of Function Matrix and its Calculus). - Xiumei Yang; Yong Guan; Zhiping Shi 002; Aixuan Wu; Qianying Zhang; Jie Zhang 074 (计算机科学, 2016)

Formalization and analysis of jacobian matrix in screw theory and its application in kinematic singularity. - Aixuan Wu; Zhiping Shi 002; Xiumei Yang; Yong Guan; Yongdong Li; Xiaoyu Song (IROS, 2017)

Formal analysis of the kinematic Jacobian in screw theory. - Zhiping Shi 002; Aixuan Wu; Xiumei Yang; Yong Guan; Yongdong Li; Xiaoyu Song (Formal Aspects Comput., 2018)

A HOL Theory of the Differential for Matrix Functions. - Yuhan Nie; Zhiping Shi 002; Aixuan Wu; Ximeng Li 003; Guohui Wang; Yong Guan (TASE, 2019)