Integration of Multiple Formal Matrix Models in Coq. - ZhengPu Shi; Gang Chen (SETTA, 2022)

CoqMatrix: Formal matrix library with multiple models in Coq. - ZhengPu Shi; Guojun Xie; Gang Chen (J. Syst. Archit., 2023)

Coq Formalization of Orientation Representation: Matrix, Euler Angles, Axis-Angle and Quaternion. - ZhengPu Shi; Gang Chen (FACS, 2024)

Formal Verification of Executable Matrix Inversion via Adjoint Matrix and Gaussian Elimination. - ZhengPu Shi; Gang Chen (PPDP, 2024)