矩阵在理论数学、工程数学以及计算机科学中都有着广泛的应用。例如飞行控制系统的设计中,矩阵被用于飞行器受力状况的描述,运动学方程的推导,以及飞行控制算法的设计。因此,矩阵算法和矩阵数学推导的正确性对这类安全关键系统的可靠性有着极大的影响。形式化方法是保障计算机系统安全可靠的一种重要方法,其中定理证明技术可用于数学公式和计算机算法的验证,是最严格、最强力的验证手段。Coq就是这样一个交互式的高阶定理证明器,它基于归纳构造演算的基本理论,具有很强的表达能力,支持丰富的逻辑系统。Coq可用于表达规范说明,构造满足规范说明的程序模型,以及对可信性要求很高的程序进行形式化验证。虽然Coq中有着丰富的定理库,但是,现有的矩阵形式化方面的几种方案却不尽人意,基于List的方案表达能力受限,基于依赖类型List的方案复杂难验证,基于函数的方案只是验证了矩阵理论,不能构造出具有具体数据的矩阵,也不能用于实际矩阵的推导验证,并且不利于从描述中提取可执行程序。本文提出了一种基于Record类型的矩阵形式化方法,它具有描述上的简明性、证明上的简单性、使用上的简便性以及程序抽取的可行性等诸方面的综合性优势。本文主要研究成果如下:首先,提出基于Record的多态类型矩阵实现方案。该方法用记录的一个List类型的域来保存矩阵数据,用类型为Prop的域来保存一个关于矩阵大小的证明。这一矩阵定义方式,既能够保证矩阵具有指定的大小,又能够利用List类型实现简单的特性。在矩阵运算函数的设计和矩阵性质证明的复杂度上都比Coq中其它矩阵验证相关工作所采用的方法更简单。其次,研究了基于函子的独立于元素类型、具有通用性的向量和矩阵的形式化方法。函子是一种参数化模块,它可以看作是从模块到模块的函数。函子的输入参数的类型被称为签名,它描述了元素模块中的数据类型、在这种类型上的运算和这些运算所需要满足的性质。基于函子的矩阵能够利用输入元素的性质来证明矩阵的性质。常规的矩阵形式化方法需要对不同类型的矩阵分别进行形式化,借助函子,可以对各类矩阵进行统一定义,并对部分矩阵性质进行统一的形式化验证。接着,在函子向量和矩阵的基础上完成了实数矩阵、复数矩阵的形式化。同时实现了函数域的形式化,并在Coquelicot库一元函数定积分的基础上实现了二元、三元函数定积分的形式化。最后在前面工作的基础上进行了函数矩阵以及函数矩阵微积分的形式化描述和部分性质的验证。最后,我们通过飞行控制系统中坐标转换矩阵和运动学方程组的验证,来展示这个矩阵库的使用。可以看出,基于Record类型的矩阵使用简单,能够满足基础矩阵运算验证的需求。